Backdoors in the Context of Learning

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.

• Type: Conference
• Year: 2009
• Where: SAT
• Authors: Bistra N. Dilkina, Carla P. Gomes, Ashish Sabharwal
• Keywords: Account Clause Learning, Hardware, Mixed Integer Programming, SAT 2009, Successful Combinatorial Reasoning