Open AccessAn integrated approach for combining BDDs and SAT provers
Author(s) -
Rolf Drechsler,
Görschwin Fey,
S. Kinder
Publication year - 2007
Publication title -
facta universitatis. series electronics and energetics/facta universitatis. series: electronics and energetics
Language(s) - English
Resource type - Journals
eISSN - 2217-5997
pISSN - 0353-3670
DOI - 10.2298/fuee0703415d
Subject(s) - binary decision diagram , computer science , boolean satisfiability problem , boolean function , satisfiability , algorithm , true quantified boolean formula , theoretical computer science , context (archaeology) , formal verification , biology , paleontology
Many formal verification tools today are based on Boolean proof techniques The two most powerful approaches in this context are Binary Decision Diagrams (BDDs) and methods based on Boolean Satisfiability (SAT). Recent studies have shown that BDDs and SAT are orthogonal, i.e. there exist problems where BDDs work well, while SAT solvers fail and vice versa. Beside this, the techniques are very different in general. E.g. SAT solvers try to find a single solution and BDDs represent all solutions in parallel. In this paper the first integrated approach is presented that combines BDDs and SAT within a single data structure. This hybrid approach combines the advantages of the two techniques, i.e. multiple solutions can be computed while the memory requirement remains small. Experimental results demonstrate the quality of the approach in comparison to BDDs and SAT solvers.