@misc{NovikovBrinkmann, author = {Novikov, Yakov and Brinkmann, Raik}, title = {Foundations of Hierarchical SAT-Solving}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-8728}, number = {05-38}, abstract = {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.}, language = {en} }