Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver

• Main Authors: Ganai, Malay K., Ashar, Pranav, Gupta, Aarti, Zhang, Lintao, Malik, Sharad
• Format: Conference Proceeding
• Language: English
• Subjects: Applied computing > Arts and humanities > Architecture (buildings) > Computer-aided design; Applied computing > Physical sciences and engineering > Engineering > Computer-aided design; Applied sciences; Electronics; Exact sciences and technology; Integrated circuits; Integrated circuits by function (including memories and processors); Semiconductor electronics. Microelectronics. Optoelectronics. Solid state devices
• ISSN: 0738-100X
• DOI: 10.1145/513918.514105

We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.