Sciweavers

Share
DAC
2004
ACM

Exploiting structure in symmetry detection for CNF

10 years 5 days ago
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...
Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2004
Where DAC
Authors Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, Igor L. Markov
Comments (0)
books