Backdoor Trees

Marko Samer, Stefan Szeider

The surprisingly good performance of modern satisfiability (SAT) solvers is usually explained by the existence of a certain "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 results. Our theoretical results are concerned with the computational 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.

Subjects: 15.7 Search; 9.2 Computational Complexity

Submitted: Apr 15, 2008

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.