Publication at Faculty of Mathematics and Physics |
2010
Abstract
We present an overview of known classes of Boolean formulae for which polynomial time algorithms for satisfiability testing (SAT) are known. We will summarize basic properties of these classes and their mutual relations with respect to inclusion.
One of these classes on which we focus our attention in particular is the class of Single Lookahead Unit Resolution formulae (SLUR). We will define a hierarchy of classes which constitutes a generalization of the SLUR class, and prove its properties.