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.

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: HoonSang Jin, Mohammad Awedh, Fabio Somenzi
• Keywords: CAV 2004, Circus, CNF Clauses, Hardware, Powerful Bdd-based Implication