SAT via Recursive Backdoors

Due to its expressiveness the SAT problem of checking whether a formula of propositional logic is satisfiable is widely used as a general problem solving framework. While SAT is computationally hard on general formulas, there exist restricted tractable classes of formulas, for which SAT solving is known to be efficient. A backdoor of a CNF formula phi to a tractable class C of formulas is a set B of variables of phi that when assigned reduces phi to a formula from C. Backdoors of small size or with a good structure, lead to efficient solutions for SAT. In our paper we introduce the new notion of recursive backdoors, which generalize backdoors and exploit the structure of formulas that can be recursively split into independent parts by partial assignments. Our generalization is motivated by the observation that independent or loosely connected components are common among real world SAT instances and many industrial solvers use value caching heuristics or component analysis in order to exploit this property. The quality of a recursive backdoor is measured by its recursive backdoor depth. Recursive backdoors of bounded depth can contain an unbounded number of variables and allow for efficient SAT solving if they are given as an input to the solver. The challenge therefore lies in the detection of recursive backdoors. For the base class of empty formulas C0, we show that recursive backdoor detection is fixed-parameter tractable and yields new tractability results for SAT.

Authors

• Nikolas Mählmann

Keywords

No keywords are indexed for this paper.