Symmetry reduction in SAT-based model checking

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.