Efficient conflict driven learning in a boolean satisfiability solver

Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik

Research output: Contribution to journalArticle

523 Scopus citations

Abstract

One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2X speedup compared with learning schemes employed in state-of-the-art SAT solvers.

Original languageEnglish (US)
Article number42
Pages (from-to)279-285
Number of pages7
JournalIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
DOIs
StatePublished - 2001

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Efficient conflict driven learning in a boolean satisfiability solver'. Together they form a unique fingerprint.

  • Cite this