Abstract
Checkers for propositional satisfiability (SAT solvers) are the most effective tools for solving important classes of industrial-scale problems (in computer-aided design of integrated circuits, planning, model checking, scheduling, cryptography, ...). One step "ahead" of SAT solvers, we encounter QBF provers. They manipulate the language of QBFs (Quantified Boolean Formulas), which adds the valuable possibility of quantifying universally over the truth value of variables (i.e. of requiring that a subformula is valid for both truth values of some variable). Such extra capability allows us to capture furhter application-relevant problems, and to obtain substantially compressed representations for classical ones (e.g. bounded model checking). In this introductory talk, we highlight the expressive difference between SAT and QBF, and we mention application-relevant problems that can be encoded into QBF. Then, we present several decision procedures for QBF, from classical DPLL-like search, to the latest solving paradigm - called "symbolic skolemization" - the first one to be expressly designed for this quantified language, with quite limited re-use or adaptation of techniques developed for SAT solvers. To conclude, a publically available system implementing this whole set of techniques - called "sKizzo" - is described, and experimental results and comparisons with other solvers are sketched.
Biography
After obtaining his PhD in 2002 at DIS (Department of Informatics and Systems Science, Univ. La Sapienza, Rome, Italy) with a thesis entitled "Bridging Refutation and Search in Propositional Satisfiability", Marco Benedetti moved to ITC-Irst (Institute for Scientific and Technological Research, Trento, Italy) where he has been working on SAT-based techniques for Model Checking. In the last few years he has focused on the theory and applications of Quantified Boolean Formulas (QBFs), a framework that allows to automate deduction in formal verification, planning, model checking, etc. He has developed many algorithms and techniques for evaluating and certifying QB formulas, all of which are implemented in the state-of-the-art solver "sKizzo". Currently, Dr. Benedetti is a Research Associate at LIFO (Laboratoire d'Informatique Fondamentale d'Orlians, France), where he works mainly on extensions of Quantified Constraint Satisfaction Problems (QCSPs), for which he has co-designed a publicly available solver called QeCode.