[PRL] Fwd: Torture chamber: Eugene Goldberg, 11/2, 2pm

[Karl Lieberherr]

Enclosed are Eugene's slides.

-- Karl

>
> ---------- Forwarded message ----------
> From: Aaron Turon <turon at ccs.neu.edu>
> Date: Sun, Nov 1, 2009 at 5:50 PM
> Subject: [PRL] Torture chamber: Eugene Goldberg, 11/2, 2pm
> To: prl at lists.ccs.neu.edu, pl-sem-jr at lists.ccs.neu.edu
>
>
> 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.
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
-------------- next part --------------
A non-text attachment was scrubbed...
Name: dagstuhl-2009.ppt
Type: application/vnd.ms-powerpoint
Size: 643072 bytes
Desc: not available
Url : http://lists.ccs.neu.edu/pipermail/prl/attachments/20091102/5b94343e/attachment-0001.ppt