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

Knowing a Backdoor Sets B for a given Sat instance, satisfiability can be decided by only examining each of the 2^|B| truth assignments of the variables in B. However, one problem is to efficiently find 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 satisfiability. 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 unsatisfiability. The upper bound of this algorithm is O(p(n) ∗ 1.427ⁿ) which is less than the currently best upper bound for deterministic algorithms for 3-SAT and MHF.