Conflict driven learning in a quantified Boolean satisfiability solver

Lintao Zhang, Sharad Malik

Research output: Contribution to journalConference articlepeer-review

125 Scopus citations

Abstract

Within the verification community, there has been a recent increase in interest in Quantified Boolean Formula evaluation (QBF) as many interesting sequential circuit verification problems can be formulated as QBF instances. A closely related research area to QBF is Boolean Satisfiability (SAT). Recent advances in SAT research have resulted in some very efficient SAT solvers. One of the critical techniques employed in these solvers is Conflict Driven Learning. In this paper, we adapt conflict driven learning for application in a QBF setting. We show that conflict driven learning can be regarded as a resolution process on the clauses. We prove that under certain conditions, tautology clauses obtained from resolution in QBF also obey the rules for implication and conflicts of regular (non-tautology) clauses; and therefore they can be treated as regular clauses and used in future search. We have implemented this idea in a new QBF solver called Quaffle and our initial experiments show that conflict driven learning can greatly speed up the solution process for most of the benchmarks we tested.

Original languageEnglish (US)
Pages (from-to)442-449
Number of pages8
JournalIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
DOIs
StatePublished - 2002
EventIEEE/ACM International Conference on Computer Aided Design (ICCAD) - San Jose, CA, United States
Duration: Nov 10 2002Nov 14 2002

All Science Journal Classification (ASJC) codes

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

Fingerprint Dive into the research topics of 'Conflict driven learning in a quantified Boolean satisfiability solver'. Together they form a unique fingerprint.

Cite this