Exploiting structure in symmetry detection for CNF

Instances of the Boolean satisfiability problem (SAT) arise in many areas of circuit design and verification. These instances are typically constructed from some human-designed artifact, and thus are likely to possess much inherent symmetry and sparsity. Previous work [4] has shown that exploiting symmetries results in vastly reduced SAT solver run times, often with the search for the symmetries themselves dominating the total SAT solving time. Our contribution is twofold. First, we dissect the algorithms behind the venerable nauty [9] package, particularly the partition refinement procedure responsible for the majority of search space pruning as well as the majority of run time overhead. Second, we present a new symmetry-detection tool, saucy, which outperforms nauty by several orders of magnitude on the large, structured CNF formulas generated from typical EDA problems. Categories and Subject Descriptors G.2.2 Discrete Mathematics--Graph algorithms. General Terms Algorithms, Verific...

• Type: Conference
• Year: 2004
• Where: DAC
• Authors: Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, Igor L. Markov
• Keywords: Boolean Satisfiability Problem, DAC 2004, Design Automation, Partition Refinement Procedure, SAT Solving Time