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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Holger Arnold
URN:urn:nbn:de:kobv:517-opus-15421
Document Type:Article
Language:English
Year of Completion: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
Dewey Decimal 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]