Recursive Backdoors for SAT

TL;DR

This paper introduces recursive backdoors for SAT, a new concept inspired by recursive decomposition, which broadens the scope of tractability beyond traditional backdoor measures.

Contribution

It proposes the novel notion of recursive backdoors and analyzes their properties, providing new tractability results for SAT problems.

Findings

Recursive backdoors generalize traditional backdoors.

Bounded recursive backdoor depth leads to efficient SAT solving.

Recursive backdoors include large, treelike backdoors with unbounded size.

Abstract

A strong backdoor in a formula $\phi$ of propositional logic to a tractable class $\mathcal{C}$ of formulas is a set $B$ of variables of $\phi$ such that every assignment of the variables in $B$ results in a formula from $\mathcal{C}$. Strong backdoors of small size or with a good structure, e.g. with small backdoor treewidth, lead to efficient solutions for the propositional satisfiability problem SAT. In this paper we propose the new notion of recursive backdoors, which is inspired by the observation that in order to solve SAT we can independently recurse into the components that are created by partial assignments of variables. The quality of a recursive backdoor is measured by its recursive backdoor depth. Similar to the concept of backdoor treewidth, recursive backdoors of bounded depth include backdoors of unbounded size that have a certain treelike structure. However, the two concepts are incomparable and our results yield new tractability results for SAT.