CirCUs is a satisfiability solver that works on a combination of an And-Inverter-Graph (AIG), Conjunctive Normal Form (CNF) clauses, and Binary Decision Diagrams (BDDs). We show how BDDs are used by CirCUs to help in the solution of SAT instances given in CNF. Specifically, the clauses are sorted by solving a hypergraph linear arrangement problem. Then they are clustered by an algorithm that strives to avoid explosion in the resulting BDD sizes. If clustering results in a single diagram, the SAT instance is solved directly. Otherwise, search for a satisfying assignment is conducted on the original clauses, enhanced with information extracted from the BDDs. We also describe a new decision variable selection heuristic that is based on recognizing that the variables involved in a conflict clause are often best treated as a related group. We present experimental results that demonstrate CirCUs’s efficiency especially for medium-size SAT instances that are hard to solve by traditional solvers based on DPLL.
Keywords for this software
References in zbMATH (referenced in 9 articles , 2 standard articles )
Showing results 1 to 9 of 9.
- Cabodi, G.; Camurati, P. E.; Mishchenko, A.; Palena, M.; Pasini, P.: SAT solver management strategies in IC3: an experimental approach (2017)
- Zeyda, Frank; Cavalcanti, Ana: Laws of mission-based programming (2015)
- Cavalcanti, Ana; Zeyda, Frank; Wellings, Andy; Woodcock, Jim; Wei, Kun: Safety-critical Java programs from \textsfCircusmodels (2013)
- Yadgar, Avi; Grumberg, Orna; Schuster, Assaf: Hybrid BDD and All-SAT method for model checking (2009)
- Drechsler, Rolf; Fey, Görschwin: Automatic test pattern generation (2006)
- Jin, Hoonsang; Somenzi, Fabio: An incremental algorithm to check satisfiability for bounded model checking (2005)
- Jin, HoonSang; Somenzi, Fabio: CirCUs: A hybrid satisfiability solver (2005)
- Pan, Guoqiang; Vardi, Moshe Y.: Symbolic techniques in satisfiability solving (2005)
- Jin, HoonSang; Awedh, Mohammad; Somenzi, Fabio: CirCUs: A satisfiability solver geared towards bounded model checking (2004)