Learning from BDDs in SAT-based bounded model checking

Aarti Gupta, Malay Ganai, Chao Wang, Zijiang Yang, Pranav Ashar

Research output: Contribution to journalConference articlepeer-review

42 Scopus citations


Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity as an alternative to BDD-based model checking techniques for finding bugs in large designs. In this paper, we explore the use of learning from BDDs, where learned clauses generated by BDD-based analysis are added to the SAT solver, to supplement its other learning mechanisms. We propose several heuristics for guiding this process, aimed at increasing the usefulness of the learned clauses, while reducing the overheads. We demonstrate the effectiveness of our approach on several industrial designs, where BMC performance is improved and the design can be searched up to a greater depth by use of BDD-based learning.

Original languageEnglish (US)
Pages (from-to)824-829
Number of pages6
JournalProceedings - Design Automation Conference
StatePublished - 2003
EventProceedings of the 40th Design Automation Conference - Anaheim, CA, United States
Duration: Jun 2 2003Jun 6 2003

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering


  • BDD learning
  • BDDs
  • Boolean Satisfiability
  • Bounded model checking
  • Learning
  • Property checking
  • SAT
  • SAT solvers


Dive into the research topics of 'Learning from BDDs in SAT-based bounded model checking'. Together they form a unique fingerprint.

Cite this