Knowing a Backdoor Sets B for a given Sat instance, satisﬁability can be decided by only examining each of the 2|B| truth assignments of the variables in B. However, one problem is to eﬃciently ﬁnd a small backdoor up to a particular size and, furthermore, if no backdoor of the desired size could be found, there is in general no chance to con- clude anything about satisﬁability. In this paper we introduce a complete deterministic algorithm for an NP-hard subclass of 3-SAT, that is also a subclass of Mixed Horn Formulas. For an instance of the described class the absence of two particular kinds of backdoor sets can be used to prove unsatisﬁability. The upper bound of this algorithm is O(p(n) ∗ 1.427n) which is less than the currently best upper bound for deterministic algorithms for 3-SAT and MHF.
A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors
Stephan Kottler, Michael Kaufmann, and Carsten Sinz
In Proc. of the 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2008), pages 161-167, Guangzhou, China