Abstrakt
Single look-ahead unit resolution (SLUR) algorithm is a nondeterministic polynomial time algorithm which for a given input formula in a conjunctive normal form (CNF) either outputs its satisfying assignment or gives up. A CNF formula belongs to the SLUR class if no sequence of nondeterministic choices causes the SLUR algorithm to give up on it.
The SLUR class is reasonably large. It is known to properly contain the well studied classes of Horn CNFs, renamable Horn CNFs, extended Horn CNFs, and CC-balanced CNFs.
Recently, it was shown, that a canonical representation of a Boolean function always belongs to the SLUR class. In this paper we extend this result by showing, that this remains true even for some representations, which are not far from the canonical one.
We also generalize the hierarchy of classes of Boolean formulae which was built on top of the CLUR class in previous paper.