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. / 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.
| Identifer | oai:union.ndltd.org:Potsdam/oai:kobv.de-opus-ubp:1542 |
| Date | January 2007 |
| Creators | Arnold, Holger |
| Publisher | Universität Potsdam, Mathematisch-Naturwissenschaftliche Fakultät. Institut für Informatik |
| Source Sets | Potsdam University |
| Language | English |
| Detected Language | German |
| Type | Article |
| Format | application/pdf |
| Rights | http://opus.kobv.de/ubp/doku/urheberrecht.php |
Page generated in 0.002 seconds