Chaff: Engineering an efficient SAT solver

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, Sharad Malik

Research output: Contribution to journalConference articlepeer-review

2194 Scopus citations

Abstract

Boolean Satisfiability is probably the most studied of combinatorial optimization/search problems. Significant effort has been devoted to trying to provide practical solutions to this problem for problem instances encountered in a range of applications in Electronic Design Automation (EDA), as well as in Artificial Intelligence (AI). This study has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. In this paper we describe the development of a new complete solver, Chaff, which achieves significant performance gains through careful engineering of all aspects of the search - especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy. Chaff has been able to obtain one to two orders of magnitude performance improvement on diffi cult SAT benchmarks in comparison with other solvers (DP or otherwise), including GRASP and SATO.

Original languageEnglish (US)
Pages (from-to)530-535
Number of pages6
JournalProceedings - Design Automation Conference
StatePublished - 2001
Event38th Design Automation Conference - Las Vegas, NV, United States
Duration: Jun 18 2001Jun 22 2001

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering

Keywords

  • Boolean satisfiability
  • Design verification

Fingerprint Dive into the research topics of 'Chaff: Engineering an efficient SAT solver'. Together they form a unique fingerprint.

Cite this