TY - GEN A1 - Novikov, Yakov A1 - Brinkmann, Raik T1 - Foundations of Hierarchical SAT-Solving N2 - 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. T3 - ZIB-Report - 05-38 KW - SAT KW - implicativity KW - verification KW - Boolean vector function KW - satisfiability KW - Bounded-Model-Checking KW - BMC KW - model KW - block KW - hierarchy Y1 - 2005 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:0297-zib-8728 ER -