As many verification and design automation problems concerning finite state hardware and software systems can be expressed as satisfiability problems for propositional logics, there is a growing demand for efficient satisfiability checkers for such logics. Application domains include combinational and sequential equivalence checking for circuits, test pattern generation, and bounded model checking. More recently, SAT solvers have become essential components in SMT solvers, where they are coupled with solvers for conjunctions of constraints over some background theory (e.g. the theory of linear arithmetic over the reals) in order to solve arbitrary Boolean combinations of such constraints. SAT solvers thus take a key role in technologies which help to master the complexity of ever larger circuits and ever more refined embedded software, which has sparked much research on enhancing their capabilities.


Conjunctive Normal Form Propositional Variable Boolean Formula Disjunctive Normal Form Unit Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Vieweg+Teubner Verlag | Springer Fachmedien Wiesbaden GmbH 2011

Authors and Affiliations

  • Christian Herde

There are no affiliations available

Personalised recommendations