BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:Symbolic Techniques in Propositional Satisfiabilit
y Solving - Moshe Y Vardi\, Rice University
DTSTART;TZID=Europe/London:20100702T140000
DTEND;TZID=Europe/London:20100702T153000
UID:TALK25135AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/25135
DESCRIPTION:Search-based techniques in propositional satisfiab
ility (SAT) solving have been enormously successfu
l\, 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-Lo
veland (DPLL) technique\, augmented with backjumpi
ng 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 inv
estigating alternative techniques. This work focus
es on symbolic techniques for SAT solving\, with t
he aim of stimulating a broader research agenda in
this area. Refutation proofs can be viewed as a s
pecial case of constraint propagation\, which is a
fundamental technique in solving constraint-satis
faction problems. The generalization lifts\, in a
uniform way\, the concept of refutation from Boole
an satisfiability problems to general constraint-s
atisfaction problems. On the one hand\, this enabl
es us to study and characterize basic concepts\, s
uch as refutation width\, using tools from finite-
model theory. On the other hand\, this enables us
to introduce new proof systems\, based on represen
tation classes\, that have not been considered up
to this point. We consider ordered binary decision
diagrams (OBDDs) as a case study of a representat
ion class for refutations\, and compare their stre
ngth to well-known proof systems\, such as resolut
ion\, the Gaussian calculus\, cutting planes\, and
Frege systems of bounded alternation-depth. In pa
rticular\, we show that refutations by ODBBs polyn
omially simulate resolution and can be exponential
ly stronger. We then describe an effort to turn OB
DD refutations into OBBD decision procedures. The
idea of this approach\, which we call `symbolic qu
antifier elimination`\, is to view an instance of
propositional satisfiability as an existentially q
uantified propositional formula. Satisfiability so
lving then amounts to quantifier elimination\; onc
e 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 o
ptimization techniques for the symbolic approach.
In comparing the symbolic approach to ZChaff\, we
evaluate scalability across a variety of classes o
f formulas. We find that no approach dominates acr
oss all classes. While ZChaff dominates for many c
lasses of formulas\, the symbolic approach is supe
rior for other classes of formulas. Finally\, we t
urn our attention to Quantified Boolean Formulas (
QBF) solving. Much recent work has gone into adapt
ing techniques that were originally developed for
SAT solving to QBF solving. In particular\, QBF so
lvers are often based on SAT solvers. Most competi
tive QBF solvers are search-based. Here we describ
e an alternative approach to QBF solving\, based o
n symbolic quantifier elimination. We extend some
symbolic approaches for SAT solving to symbolic QB
F solving\, using various decision-diagram formali
sms such as OBDDs and ZDDs. In both approaches\, Q
BF formulas are solved by eliminating all their qu
antifiers. Our first solver\, QMRES\, maintains a
set of clauses represented by a ZDD and eliminates
quantifiers via multi-resolution. Our second solv
er\, QBDD\, maintains a set of OBDDs\, and elimina
te quantifiers by applying them to the underlying
OBDDs. We compare our symbolic solvers to several
competitive search-based solvers. We show that QBD
D is not competitive\, but QMRESS compares favorab
ly with search-based solvers on various benchmarks
consisting of non-random formulas.
LOCATION:Small public lecture room\, Microsoft Research Ltd
\, 7 J J Thomson Avenue (Off Madingley Road)\, Cam
bridge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR