Foundations of Hierarchical SAT-Solving
Please always quote using this URN: urn:nbn:de:0297-zib-8728
- The theory of hierarchical Boolean satisfiability (SAT) solving proposed in this paper is based on a strict axiomatic system and introduces a new important notion of implicativity. The theory makes evident that increasing implicativity is the core of SAT-solving. We provide a theoretical basis for increasing the implicativity of a given SAT instance and for organizing SAT-solving in a hierarchical way. The theory opens a new domain of research: SAT-model construction. Now quite different mathematical models can be used within practical SAT-solvers. The theory covers many advanced techniques such as circuit-oriented SAT-solving, mixed BDD/CNF SAT-solving, merging gates, using pseudo-Boolean constraints, using state machines for representation of Boolean functions, arithmetic reasoning, and managing don t cares. We believe that hierarchical SAT-solving is a cardinal direction of research in practical SAT-solving.
| Author: | Yakov Novikov, Raik Brinkmann |
|---|---|
| Document Type: | ZIB-Report |
| Tag: | BMC; Boolean vector function; Bounded-Model-Checking; SAT; block; hierarchy; implicativity; model; satisfiability; verification |
| MSC-Classification: | 06-XX ORDER, LATTICES, ORDERED ALGEBRAIC STRUCTURES [See also 18B35] / 06Exx Boolean algebras (Boolean rings) [See also 03G05] / 06E30 Boolean functions [See also 94C10] |
| 94-XX INFORMATION AND COMMUNICATION, CIRCUITS / 94Cxx Circuits, networks / 94C10 Switching theory, application of Boolean algebra; Boolean functions [See also 06E30] | |
| Date of first Publication: | 2005/08/03 |
| Series (Serial Number): | ZIB-Report (05-38) |
| ZIB-Reportnumber: | 05-38 |
