Třídy Booleovských formulí s efektivně řešitelným SATem.

This work studies classes of Boolean formulae with polynomially solvable satsiability problem (SAT). It investigates the behavior of these classes with respect to basic operation with formulae (variable and literal complementation, deletition of a literal or a clause, partial assignment and joining...

Full description

Bibliographic Details
Main Author: Vlček, Václav
Other Authors: Kučera, Petr
Format: Dissertation
Language:Czech
Published: 2009
Online Access:http://www.nusl.cz/ntk/nusl-286191
Description
Summary:This work studies classes of Boolean formulae with polynomially solvable satsiability problem (SAT). It investigates the behavior of these classes with respect to basic operation with formulae (variable and literal complementation, deletition of a literal or a clause, partial assignment and joining formulae). Furthermore the work studies recognition problems for a formula and a given class of functions, satisability testing, and mutual relations of the studied classes with respect to inclusion.