A linearized DPLL calculus with learning
- 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.
MetadatenAuthor details: | Holger Arnold |
---|
URN: | urn:nbn:de:kobv:517-opus-15421 |
---|
Publication type: | Article |
---|
Language: | English |
---|
Publication year: | 2007 |
---|
Publishing institution: | Universität Potsdam |
---|
Release date: | 2007/11/02 |
---|
Tag: | Automatisches Beweisen; DPLL; Klausellernen; SAT Automated Theorem Proving; Clause Learning; DPLL; SAT |
---|
Organizational units: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
---|
DDC classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
---|
MSC classification: | 03-XX MATHEMATICAL LOGIC AND FOUNDATIONS / 03Bxx General logic / 03B05 Classical propositional logic |
---|
| 03-XX MATHEMATICAL LOGIC AND FOUNDATIONS / 03Bxx General logic / 03B35 Mechanization of proofs and logical operations [See also 68T15] |
---|
| 68-XX COMPUTER SCIENCE (For papers involving machine computations and programs in a specific mathematical area, see Section {04 in that areag 68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) / 68Txx Artificial intelligence / 68T15 Theorem proving (deduction, resolution, etc.) [See also 03B35] |
---|