QBF modeling: exploiting player symmetry for simplicity and efficiency
MetadataShow full item record
Quantified Boolean Formulas (QBFs) present the next big challenge for automated propositional reasoning. Not surprisingly, most of the present day QBF solvers are extensions of successful propositional satisfiability algorithms (SAT solvers). They directly integrate the lessons learned from SAT research, thus avoiding re-inventing the wheel. In particular, they use the standard conjunctive normal form (CNF) augmented with layers of variable quantification for modeling tasks as QBF. We argue that while CNF is well suited to “existential reasoning” as demonstrated by the success of modern SAT solvers, it is far from ideal for “universal reasoning” needed by QBF. The CNF restriction imposes an inherent asymmetry in QBF and artificially creates issues that have led to complex solutions, which, in retrospect, were unnecessary and sub-optimal. We take a step back and propose a new approach to QBF modeling based on a game-theoretic view of problems and on a dual CNF-DNF (disjunctive normal form) representation that treats the existential and universal parts of a problem symmetrically. It has several advantages: (1) it is generic, compact, and simpler, (2) unlike fully nonclausal encodings, it preserves the benefits of pure CNF and leverages the support for DNF already present in many QBF solvers, (3) it doesn’t use the so-called indicator variables for conversion into CNF, thus circumventing the associated illegal search space issue, and (4) our QBF solver based on the dual encoding (Duaffle) consistently outperforms the best solvers by two orders of magnitude on a hard class of benchmarks, even without using standard learning techniques.
Is part ofLecture Notes in Computer Science, 2006, vol. 4121, p. 382-395
European research projects
Showing items related by title, author, creator and subject.
Ansótegui Gil, Carlos José; Bonet, Maria Luisa; Levy, Jordi (Elsevier, 2013)Many industrial optimization problems can be translated to MaxSAT. Although the general problem is NP hard, like SAT, many practical problems may be solved using modern MaxSAT solvers. In this paper we present several ...
Ansótegui Gil, Carlos José; Bonet, Maria Luisa; Giráldez-Cru, Jesús; Levy, Jordi (Springer Verlag, 2014)Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit ...
Ansótegui Gil, Carlos José; Larrubia, Jose; Li, Chu-Min; Manyà Serres, Felip (Springer Verlag, 2007)We show that we can design and implement extremely efficient variable selection heuristics for SAT solvers by identifying, in Boolean clause databases, sets of Boolean variables that model the same multivalued variable ...