Talk by Marco Benedetti:
QBF: Departing from the Search Paradigm
Date : Friday, February 23 2007
Time : 3-4pm
Room : PT 266
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. Such extra capability allows us to capture further application-relevant problems, and to obtain substantially compressed representations for classical ones (e.g. bounded model checking). Unquestionably, the most effective complete method to decide SAT is backtracking search (the “DPLL” method). The same was true of QBF, until 2004. Since then, several alternative decision procedures have been proposed which seem to tarnish the unrivaled reputation of the “search paradigm” in propositional reasoning. When universal quantifiers enter the game, alternative forms of reasoning which are more abstract than brute search gain credibility. In this seminar, we discuss the algorithms and techniques employed by a state-of-the-art QBF solver (sKizzo) which does its best to eschew “search”. Among these techniques we mention: quantifier elimination, symbolic skolemization, and abstract branching. Experimental results and applications to real-world cases are also discussed, together with the issues in certifying the correctness of solvers’ answers.
Speaker’s 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 eduction 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’Orléans, 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.
