ZIB-Report
Refine
Year of publication
- 2005 (1)
Document Type
- ZIB-Report (1)
Language
- English (1)
Has Fulltext
- yes (1)
Is part of the Bibliography
- no (1)
Keywords
- BMC (1)
- Boolean vector function (1)
- Bounded-Model-Checking (1)
- SAT (1)
- block (1)
- hierarchy (1)
- implicativity (1)
- model (1)
- satisfiability (1)
- verification (1)
Institute
- ZIB Allgemein (1)
05-38
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.