Sciweavers

Share
CAV
2004
Springer

CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking

11 years 3 months ago
CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking
Abstract. CirCUs is a satisfiability solver that works on a combination of AndInverter-Graph, CNF clauses, and BDDs. It has been designed to work well with bounded model checking. It takes as inputs a Boolean circuit (e.g., the model unrolled k times) and an optional set of additional constraints (for instance, requesting that a solution correspond to a simple path) in the form of CNF clauses or BDDs. The algorithms in CirCUs take advantage of the mixed representation by applying powerful BDD-based implication algorithms, and decision heuristics that are objective-driven. CirCUs supports incremental SAT solving, early termination checks, and other analyses of the model that translate into SAT. Experimental results demonstrate CirCUs's efficiency.
HoonSang Jin, Mohammad Awedh, Fabio Somenzi
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CAV
Authors HoonSang Jin, Mohammad Awedh, Fabio Somenzi
Comments (0)
books