Extending DPLL for Pseudo-Boolean Constraints
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.
KeywordsConjunctive Normal Form Propositional Variable Boolean Formula Disjunctive Normal Form Unit Clause
Unable to display preview. Download preview PDF.