Abstrakt
SLUR is a class of the CNF formulae on which the single lookahead unit resolution algorithm for satisfiability (SAT) testing never fails. It is known that the SLUR class contains classes of Horn, hidden Horn, (hidden) extended Horn and balanced formulae as a subclass.
In recent paper it was proven that the SLUR class contains all canonical formulae. In this paper we will extend this result by showing it suffices that all prime implicates can be derived in one resolution step from input formula.
We will also generalize previous hierarchy called SLUR(i) which is built on top of the SLUR class.