BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Symbolic Techniques in Propositional Satisfiability Solving - Mosh
 e Y Vardi\, Rice University
DTSTART:20100702T130000Z
DTEND:20100702T143000Z
UID:TALK25135@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Search-based techniques in propositional satisfiability (SAT) 
 solving have been enormously successful\, leading to what is becoming know
 n as the ``SAT Revolution`. Essentially all state-of-the-art SAT solvers a
 re based on the Davis-Putnam-Logemann-Loveland (DPLL) technique\, augmente
 d 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 investiga
 ting alternative techniques. This work focuses on symbolic techniques for 
 SAT solving\, with the aim of stimulating a broader research agenda in thi
 s area. Refutation proofs can be viewed as a special case of constraint pr
 opagation\, which is a fundamental technique in solving constraint-satisfa
 ction problems. The generalization lifts\, in a uniform way\, the concept 
 of refutation from Boolean satisfiability problems to general constraint-s
 atisfaction problems. On the one hand\, this enables us to study and chara
 cterize basic concepts\, such as refutation width\, using tools from finit
 e-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 thei
 r strength to well-known proof systems\, such as resolution\, the Gaussian
  calculus\, cutting planes\, and Frege systems of bounded alternation-dept
 h. 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 a
 pproach\, which we call `symbolic quantifier elimination`\, is to view an 
 instance of propositional satisfiability as an existentially quantified pr
 opositional formula. Satisfiability solving then amounts to quantifier eli
 mination\; once all quantifiers have been eliminated we are left with eith
 er 1 or 0. Our goal here is to study the effectiveness of symbolic quantif
 ier elimination as an approach to satisfiability solving. To that end\, we
  conduct a direct comparison with the DPLL-based ZChaff\, as well as evalu
 ate a variety of optimization techniques for the symbolic approach. In com
 paring 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 sym
 bolic approach is superior for other classes of formulas. Finally\, we tur
 n 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 descr
 ibe an alternative approach to QBF solving\, based on symbolic quantifier 
 elimination. We extend some symbolic approaches for SAT solving to symboli
 c QBF solving\, using various decision-diagram formalisms such as OBDDs an
 d ZDDs. In both approaches\, QBF formulas are solved by eliminating all th
 eir quantifiers. Our first solver\, QMRES\, maintains a set of clauses rep
 resented by a ZDD and eliminates quantifiers via multi-resolution. Our sec
 ond solver\, QBDD\, maintains a set of OBDDs\, and eliminate quantifiers b
 y applying them to the underlying OBDDs. We compare our symbolic solvers t
 o several competitive search-based solvers. We show that QBDD is not compe
 titive\, but QMRESS compares favorably with search-based solvers on variou
 s benchmarks consisting of non-random formulas.
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR