SAT 2009
Backdoors in the Context of Learning
Abstract
Abstract The concept of backdoor variables has been introduced as a structural property of combinatorial problems that provides insight into the surprising ability of modern satisfiability (SAT) solvers to tackle extremely large instances. This concept is, however, oblivious to “learning” during search—a key feature of successful combinatorial reasoning engines for SAT, mixed integer programming (MIP), etc. We extend the notion of backdoors to the context of learning during search. We prove that the smallest backdoors for SAT that take into account clause learning and order-sensitivity of branching can be exponentially smaller than “traditional” backdoors. We also study the effect of learning empirically.
Authors
Keywords
No keywords are indexed for this paper.
Context
- Venue
- International Conference on Theory and Applications of Satisfiability Testing
- Archive span
- 2003-2025
- Indexed papers
- 824
- Paper id
- 492773374892135685