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

Malay K. Ganai, Lintao Zhang, Pranav Ashar, Aarti Gupta, Sharad Malik

Research output: Contribution to journalArticle

84 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages (from-to)747-750
Number of pages4
JournalProceedings - Design Automation Conference
DOIs
StatePublished - 2002

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering

Keywords

  • Boolean constraint propagation (BCP)
  • Boolean satisfiability (SAT)
  • Bounded model checking (BMC)
  • Conjunctive normal form (CNF)

Fingerprint Dive into the research topics of 'Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver'. Together they form a unique fingerprint.

  • Cite this