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 circuitoriented decision ordering technique (J-frontier), our solver can constantly outperform the CNF ones for more than 15+ times. With the great flexibility on the circuitbased data structure, our solver can serve as a solid foundation for the general SAT researc...

• Type: Conference
• Year: 2007
• Where: DATE
• Authors: Chi-An Wu, Ting-Hao Lin, Chih-Chun Lee, Chung-Yang Huang
• Keywords: Circuit Netlist Structure, Data Structure, DATE 2007, Efficient Boolean Constraint, Hardware