[PL-sem-jr] Torture chamber: Eugene Goldberg, 11/2, 2pm

[Aaron Turon]

Eugene Goldberg is giving a practice talk for Dagstuhl seminar:
Monday, 11/2, 2-3:30
WVH166

Boundary point elimination: a path to structure aware SAT-solvers.

Taking into account formula's structure is extremely important for
making SAT-solvers scalable. One of the problems here is that a SAT
solver with conflict  clause  learning creates its own structure
(induced by conflicts) that may have  little to  do with the real
structure of the formula.  In particular, a single resolution is
"meaningless" in a  SAT-solver based on the DPLL procedure unless it
is used in deriving a conflict clause. We describe a SAT-algorithm
called IBP (Interpolation with Boundary Point elimination) that is not
conflict driven and so  builds a proof from "individual" resolution
operations.  We show that IBP compares favorably with
state-of-the-art SAT-solvers on narrow formulas. We  also argue  that
IBP  can be viewed as a generalization of the  conflict clause
generating procedure and so can be used to advance the state of the
art in SAT-solvers based on the DPLL  procedure.