Backdoor Trees

The surprisingly good performance of modern satisfiability (SAT) solvers is usually explained by the existence of a cer-tain “hidden structure ” in real-world instances. We introduce the notion of backdoor trees as an indicator for the presence of a hidden structure. Backdoor trees refine the notion of strong backdoor sets, taking into account the relationship between backdoor variables. We present theoretical and empirical re-sults. Our theoretical results are concerned with the compu-tational complexity of detecting small backdoor trees. With our empirical results we compare the size of backdoor trees against the size of backdoor sets for real-world SAT instances and random 3SAT instances of various density. The results indicate that backdoor trees amplify the properties that have been observed for backdoor sets