1428
2007
eng
article
0
2007-11-02
--
--
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.
urn:nbn:de:kobv:517-opus-15421
1542
Holger Arnold
deu
uncontrolled
SAT
deu
uncontrolled
DPLL
deu
uncontrolled
Klausellernen
deu
uncontrolled
Automatisches Beweisen
eng
uncontrolled
SAT
eng
uncontrolled
DPLL
eng
uncontrolled
Clause Learning
eng
uncontrolled
Automated Theorem Proving
Datenverarbeitung; Informatik
Classical propositional logic
Mechanization of proofs and logical operations [See also 68T15]
Theorem proving (deduction, resolution, etc.) [See also 03B35]
open_access
Institut für Informatik und Computational Science
Universität Potsdam
https://publishup.uni-potsdam.de/files/1428/arnold_aufsatz.pdf
2728
2009
eng
preprint
0
2009-03-10
--
--
A linearized DPLL calculus with clause learning (2nd, revised version)
Many formal descriptions of DPLL-based SAT algorithms either do not include all essential proof techniques applied by modern SAT solvers or are bound to particular heuristics or data structures. This makes it difficult to analyze proof-theoretic properties or the search complexity of these algorithms. In this paper we try to improve this situation by developing a nondeterministic proof calculus that models the functioning of SAT algorithms based on the DPLL calculus with clause learning. This calculus is independent of implementation details yet precise enough to enable a formal analysis of realistic DPLL-based SAT algorithms.
Viele formale Beschreibungen DPLL-basierter SAT-Algorithmen enthalten entweder nicht alle wesentlichen Beweistechniken, die in modernen SAT-Solvern implementiert sind, oder sind an bestimmte Heuristiken oder Datenstrukturen gebunden. Dies erschwert die Analyse beweistheoretischer Eigenschaften oder der Suchkomplexität derartiger Algorithmen. Mit diesem Artikel versuchen wir, diese Situation durch die Entwicklung eines nichtdeterministischen Beweiskalküls zu verbessern, der die Arbeitsweise von auf dem DPLL-Kalkül basierenden SAT-Algorithmen mit Klausellernen modelliert. Dieser Kalkül ist unabhängig von Implementierungsdetails, aber dennoch präzise genug, um eine formale Analyse realistischer DPLL-basierter SAT-Algorithmen zu ermöglichen.
urn:nbn:de:kobv:517-opus-29080
2908
Keine öffentliche Lizenz: Unter Urheberrechtsschutz
Holger Arnold
deu
uncontrolled
Automatisches Beweisen
deu
uncontrolled
Logikkalkül
deu
uncontrolled
SAT
deu
uncontrolled
DPLL
deu
uncontrolled
Klausellernen
eng
uncontrolled
automated theorem proving
eng
uncontrolled
logical calculus
eng
uncontrolled
SAT
eng
uncontrolled
DPLL
eng
uncontrolled
clause learning
Datenverarbeitung; Informatik
Classical propositional logic
Mechanization of proofs and logical operations [See also 68T15]
Theorem proving (deduction, resolution, etc.) [See also 03B35]
open_access
Institut für Informatik und Computational Science
Universität Potsdam
https://publishup.uni-potsdam.de/files/2728/linearized_DPLL.pdf