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.

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-29080
Document Type:Preprint
Language:English
Year of Completion:2009
Publishing Institution:Universität Potsdam
Release Date:2009/03/10
Tag:Automatisches Beweisen; DPLL; Klausellernen; Logikkalkül; SAT
DPLL; SAT; automated theorem proving; clause learning; logical calculus
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]
Licence (German):License LogoKeine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht