QuteSAT: A Robust Circuit-based SAT Solver for Complex Circuit Structure

The paper proposes 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. The 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. The authors 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 75+ 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