CirCUs swMATH ID: 128 Software Authors: Jin, HoonSang; Somenzi, Fabio Description: 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. Homepage: http://vlsi.colorado.edu/~vis/releaseNotes/releaseNotes-2.3.html Related Software: Chaff; CUDD; zChaff; BerkMin; Circus; ZRC; Z; SBSAT; SATIRE; SATO; MiniSat; nuXmv; ArcAngelC; SATORI; HANNIBAL; PASSAT; SOCRATES; HITEC; FORCE Cited in: 9 Documents Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year CirCUs: A hybrid satisfiability solver. Zbl 1122.68606Jin, HoonSang; Somenzi, Fabio 2005 CirCUs: A satisfiability solver geared towards bounded model checking. Zbl 1103.68625Jin, HoonSang; Awedh, Mohammad; Somenzi, Fabio 2004 all top 5 Cited by 19 Authors 3 Jin, HoonSang 3 Somenzi, Fabio 2 Cavalcanti, Ana 2 Zeyda, Frank 1 Awedh, Mohammad 1 Cabodi, Gianpiero 1 Camurati, P. E. 1 Drechsler, Rolf 1 Fey, Görschwin 1 Grumberg, Orna 1 Palena, Marco 1 Pan, Guoqiang 1 Pasini, Paolo 1 Schuster, Assaf 1 Vardi, Moshe Ya’akov 1 Wei, Kun 1 Wellings, Andy 1 Woodcock, James C. P. 1 Yadgar, Avi Cited in 4 Serials 1 Journal of Automated Reasoning 1 Formal Aspects of Computing 1 Real-Time Systems 1 Formal Methods in System Design Cited in 2 Fields 9 Computer science (68-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year