Institut für Informatik und Computational Science
Refine
Has Fulltext
- yes (1)
Year of publication
- 2007 (1) (remove)
Document Type
- Article (1)
Language
- English (1)
Is part of the Bibliography
- no (1)
Keywords
- DPLL (1) (remove)
Institute
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.