Symmetry reduction in SAT-based model checking

Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip

Research output: Contribution to journalConference article

6 Scopus citations

Abstract

The major challenge facing model checking is the state explosion problem. One technique to alleviate this is to apply symmetry reduction; this exploits the fact that many sequential systems consist of interchangeable components, and thus it may suffice to search a reduced version of the symmetric state space. Symmetry reduction has been shown to be an effective technique in both explicit and symbolic model checking with Binary Decision Diagrams (BDDs). In recent years, SAT-based model checking has been shown to be a promising alternative to BDD-based model checking. In this paper, we describe a symmetry reduction algorithm for SAT-based unbounded model checking (UMC) using circuit cofactoring. Our method differs from the previous efforts in using symmetry mainly in that we do not require converting any set of states to its representative or orbit set of states except for the set of initial states. This leads to significant simplicity in the implementation of symmetry reduction in model checking. Experimental results show that using our symmetry reduction approach improves the performance of SAT-based UMC due to both the reduced state space and simplification in the resulting SAT problems.

Original languageEnglish (US)
Pages (from-to)125-138
Number of pages14
JournalLECTURE NOTES IN COMPUTER SCIENCE
Volume3576
DOIs
StatePublished - 2005
Event17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom
Duration: Jul 6 2005Jul 10 2005

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Symmetry reduction in SAT-based model checking'. Together they form a unique fingerprint.

  • Cite this