BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
Symbolic Techniques in Propositional Satisfiability Solving
STATUS:CONFIRMED
ATTENDEE;CN="Moshe Y. Vardi
":
MAILTO:no@spam.com
DESCRIPTION:
Search-based techniques in propositional satisfiability (SAT
) solving have been enormously successful\, leading to what
is becoming known as the "SAT Revolution". Essentially all s
tate-of-the-art SAT solvers are based on the Davis-Putnam-Lo
gemann-Loveland (DPLL) technique\, augmented with backjumpin
g and conflict learning. Much of current research in this ar
ea involves refinements and extensions of the DPLL technique
. Yet\, due to the impressive success of DPLL\, little effor
t has gone into investigating alternative techniques. This w
ork focuses on symbolic techniques for SAT solving\, with th
e aim of stimulating a broader research agenda in this area.
Refutation proofs can be viewed as a special case of constr
aint propagation\, which is a fundamental technique in solvi
ng constraint-satisfaction problems. The generalization lift
s\, in a uniform way\, the concept of refutation from Boolea
n satisfiability problems to general constraint-satisfaction
problems. On the one hand\, this enables us to study and ch
aracterize basic concepts\, such as refutation width\, using
tools from finite-model theory. On the other hand\, this en
ables us to introduce new proof systems\, based on represent
ation classes\, that have not been considered up to this poi
nt. 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 a
s resolution\, the Gaussian calculus\, cutting planes\, and
Frege systems of bounded alternation-depth. In particular\,
we show that refutations by ODBBs polynomially simulate reso
lution and can be exponentially stronger. We then describe a
n effort to turn OBDD refutations into OBBD decision procedu
res. The idea of this approach\, which we call "symbolic qua
ntifier elimination"\, is to view an instance of proposition
al satisfiability as an existentially quantified proposition
al formula. Satisfiability solving then amounts to quantifie
r elimination; once all quantifiers have been eliminated we
are left with either 1 or 0. Our goal here is to study the e
ffectiveness of symbolic quantifier elimination as an approa
ch to satisfiability solving. To that end\, we conduct a dir
ect comparison with the DPLL-based ZChaff\, as well as evalu
ate a variety of optimization techniques for the symbolic ap
proach. In comparing the symbolic approach to ZChaff\, we ev
aluate 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 symboli
c approach is superior for other classes of formulas. Finall
y\, we turn our attention to Quantified Boolean Formulas (QB
F) solving. Much recent work has gone into adapting techniqu
es that were originally developed for SAT solving to QBF sol
ving. In particular\, QBF solvers are often based on SAT sol
vers. 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 app
roaches for SAT solving to symbolic QBF solving\, using vari
ous decision-diagram formalisms such as OBDDs and ZDDs. In b
oth approaches\, QBF formulas are solved by eliminating all
their quantifiers. Our first solver\, QMRES\, maintains a se
t 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 sear
ch-based solvers on various benchmarks consisting of non-ran
dom formulas.
DTSTART;TZID=Europe/Paris:20101103T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201011031
100
UID:LSVsemLSV.201011031100@lsv.ens-cachan.fr
LOCATION:Salle de ConfĂ©rence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR