Moshe Vardi visiting Webdam
Moshe Y. Vardi is visiting Webdam Wednesday 3 November. He is Karen Ostrum George Professor in Computational Engineering and Director of the Computer and Information Technology Institute ((Rice University, Houston, Texas). His interests focus on applications of logic to computer science, including database theory, finite-model theory, knowledge in multi-agent systems, computer-aided verification and reasoning, and teaching logic across the curriculum. He will present his work on propositional satisfiability in the meeting room of ENS Cachan (Pavillon des Jardins) at 11:00am.
Title: Symbolic Techniques in Propositional Satisfiability Solving
Abstract: Search-based techniques in propositional satisfiability (SAT) solving have been enormously successful, leading to what is becoming known as the “SAT Revolution”. Essentially all state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) technique, augmented with backjumping and conflict learning. Much of current research in this area involves refinements and extensions of the DPLL technique. Yet, due to the impressive success of DPLL, little effort has gone into investigating alternative techniques. This work focuses on symbolic techniques for SAT solving, with the aim of stimulating a broader research agenda in this area.
Refutation proofs can be viewed as a special case of constraint propagation, which is a fundamental technique in solving constraint-satisfaction problems. The generalization lifts, in a uniform way, the concept of refutation from Boolean satisfiability problems to general constraint-satisfaction problems. On the one hand, this enables us to study and characterize basic concepts, such as refutation width, using tools from finite-model theory. On the other hand, this enables us to introduce new proof systems, based on representation classes, that have not been considered up to this point. We consider ordered binary decision diagrams (OBDDs) as a case study of a representation class for refutations, and compare their strength to well-known proof systems, such as resolution, the Gaussian calculus, cutting planes, and Frege systems of bounded alternation-depth. In particular, we show that refutations by ODBBs polynomially simulate resolution and can be exponentially stronger.
We then describe an effort to turn OBDD refutations into OBBD decision procedures. The idea of this approach, which we call “symbolic quantifier elimination”, is to view an instance of propositional satisfiability as an existentially quantified propositional formula. Satisfiability solving then amounts to quantifier elimination; once all quantifiers have been eliminated we are left with either 1 or 0. Our goal here is to study the effectiveness of symbolic quantifier elimination as an approach to satisfiability solving. To that end, we conduct a direct comparison with the DPLL-based ZChaff, as well as evaluate a variety of optimization techniques for the symbolic approach. In comparing the symbolic approach to ZChaff, we evaluate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of formulas, the symbolic approach is superior for other classes of formulas.
Finally, we turn our attention to Quantified Boolean Formulas (QBF) solving. Much recent work has gone into adapting techniques that were originally developed for SAT solving to QBF solving. In particular, QBF solvers are often based on SAT solvers. Most competitive QBF solvers are search-based. Here we describe an alternative approach to QBF solving, based on symbolic quantifier elimination. We extend some symbolic approaches for SAT solving to symbolic QBF solving, using various decision-diagram formalisms such as OBDDs and ZDDs. In both approaches, QBF formulas are solved by eliminating all their quantifiers. Our first solver, QMRES, maintains a set of clauses represented by a ZDD and eliminates quantifiers via multi-resolution. Our second solver, QBDD, maintains a set of OBDDs, and eliminate quantifiers by applying them to the underlying OBDDs. We compare our symbolic solvers to several competitive search-based solvers. We show that QBDD is not competitive, but QMRESS compares favorably with search-based solvers on various benchmarks consisting of non-random formulas.