Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Finding Small Backdoors in SAT Instances
verfasst von : Zijie Li, Peter van Beek
Erschienen in: Advances in Artificial Intelligence
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Although propositional satisfiability (SAT) is NP-complete, state-of-the-art SAT solvers are able to solve large, practical instances. The concept of backdoors has been introduced to capture structural properties of instances. A backdoor is a set of variables that, if assigned correctly, leads to a polynomial-time solvable sub-problem. In this paper, we address the problem of finding all small backdoors, which is essential for studying value and variable ordering mistakes. We discuss our definition of sub-solvers and propose algorithms for finding backdoors. We experimentally compare our proposed algorithms to previous algorithms on structured and real-world instances. Our proposed algorithms improve over previous algorithms for finding backdoors in two ways. First, our algorithms often find smaller backdoors. Second, our algorithms often find a much larger number of backdoors.