OPUS - A linearized DPLL calculus with learning

Eingang zum Volltext

Home | Suche | Browsen

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:kobv:517-opus-15421
URL: http://opus.kobv.de/ubp/volltexte/2007/1542/

Arnold, Holger

A linearized DPLL calculus with learning

pdf-Format:

Dokument 1.pdf (486 KB) (SHA-1:f9037785e5086f2f940df92a3232960c7684822e)

Kurzfassung auf Englisch

This paper describes the proof calculus LD for clausal propositional logic,
which is a linearized form of the well-known DPLL calculus extended by clause
learning. It is motivated by the demand to model how current SAT solvers
built on clause learning are working, while abstracting from decision
heuristics and implementation details. The calculus is proved sound and
terminating. Further, it is shown that both the original DPLL calculus and
the conflict-directed backtracking calculus with clause learning, as it is
implemented in many current SAT solvers, are complete and proof-confluent
instances of the LD calculus.

Kurzfassung auf Deutsch

Dieser Artikel beschreibt den Beweiskalkül LD für aussagenlogische Formeln in
Klauselform. Dieser Kalkül ist eine um Klausellernen erweiterte linearisierte
Variante des bekannten DPLL-Kalküls. Er soll dazu dienen, das Verhalten von
auf Klausellernen basierenden SAT-Beweisern zu modellieren, wobei von
Entscheidungsheuristiken und Implementierungsdetails abstrahiert werden soll.
Es werden Korrektheit und Terminierung des Kalküls bewiesen. Weiterhin wird
gezeigt, dass sowohl der ursprüngliche DPLL-Kalkül als auch der
konfliktgesteuerte Rücksetzalgorithmus mit Klausellernen, wie er in vielen
aktuellen SAT-Beweisern implementiert ist, vollständige und beweiskonfluente
Spezialisierungen des LD-Kalküls sind.

Freie Schlagwörter (deutsch): SAT , DPLL , Klausellernen , Automatisches Beweisen

Freie Schlagwörter (englisch): SAT , DPLL , Clause Learning , Automated Theorem Proving

MSC - Klassifikation 03B05 , 03B35 , 68T15

Institut: Institut für Informatik

DDC-Sachgruppe: Informatik

Dokumentart: b Aufsatz

Sprache: Englisch

Erstellungsjahr: 2007

Publikationsdatum: 02.11.2007

Ihr Kontakt für Fragen und Anregungen:
Universitätsbibliothek Potsdam