[Date Prev][Date Next][Date Index]

Vortragsankündigung Johannes Fichte: "SAT Solvers and Width-Bounded Resolution"

Der Arbeitsbereich Datenbanken & AI des Instituts für
Informationssysteme lädt zum folgenden Vortrag ein:


Johannes Fichte:  http://www2.informatik.hu-berlin.de/~fichte/

DATUM: Freitag, 16. Oktober 2009
ZEIT:  10:00 Uhr s.t.
ORT:   Seminarraum 184/2, Stiege 3, 3.Stock, Favoritenstr. 9-11

TITLE: SAT Solvers and Width-Bounded Resolution

The development of what can be called "modern" SAT solving techniques
can be traced back to at least the mid 1990's. The introduction of
practically feasible clause learning layed the foundation for several
further techniques and a new design of the implmentations. This spawned
tremendous gains in the efficency of SAT solvers. That is why they are
widely used in many applications. Among these are, for example,
microporocessor verification and bounded model checking, which often
require the solution of inputs with hundreds of thousands of variables.

The fact that SAT solvers are able to handle such huge formulas seems to
contradict the well-known intractablity of the SAT problem. We propose
an algorithmic view, relating efficient solvability by a SAT solver to
bounded width resolution. As a conclusion this enables us to show that
SAT solvers are able to handle CNF formulas of bounded treewidth in
polynomial time. On the experimental side, we give evidence for the
claim that this theoretical result describes real world solvers.

This is joint work with Albert Atserias and Marc Thurley.

Mit Unterstützung des Wolfgang-Pauli-Instituts und des Zentrums für