Institut für Informatik und Computational Science
Refine
Document Type
- Preprint (5) (remove)
Language
- English (5)
Keywords
- Automatisches Beweisen (1)
- DPLL (1)
- Klausellernen (1)
- Logikkalkül (1)
- SAT (1)
- automated theorem proving (1)
- clause learning (1)
- logical calculus (1)
Institute
Untitled
(2011)
Simplicity is a mindset, a way of looking at solutions, an extremely wide-ranging philosophical stance on the world, and thus a deeply rooted cultural paradigm. The culture of "less" can be profoundly disruptive, cutting out existing "standard" elements from products and business models, thereby revolutionizing entire markets.
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.