QuteSAT: a robust circuit-based SAT solver for complex circuit structure. We propose a robust circuit-based Boolean Satisfiability (SAT) solver, QuteSAT, that can be applied to complex circuit netlist structure. Several novel techniques are proposed in this paper, including: (1) a generic watching scheme on general gate types for efficient Boolean Constraint Propagation (BCP), (2) an implicit implication graph representation for efficient learning, and (3) careful engineering on the most advanced SAT algorithms for the circuit-based data structure. Our experimental results show that our baseline solver, without taking the advantage of the circuit information, can achieve the same performance as the fastest Conjunctive Normal Form (CNF)-based solvers. We also demonstrate that by applying a simple circuit-oriented decision ordering technique (J-frontier), our solver can constantly outperform the CNF ones for more than 15+ times. With the great flexibility on the circuit-based data structure, our solver can serve as a solid foundation for the general SAT research in the future.

This software is also peer reviewed by journal TOMS.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 3 articles )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Schwerdtfeger, Konrad W.: The connectivity of Boolean satisfiability: dichotomies for formulas and circuits (2017)
  2. Egly, Uwe; Haller, Leopold: A SAT solver for circuits based on the tableau method (2010) ioport
  3. Goultiaeva, Alexandra; Iverson, Vicki; Bacchus, Fahiem: Beyond CNF: a circuit-based QBF solver (2009)