Shatter: efficient symmetry-breaking for Boolean satisfiability

Boolean satisfiability (SAT) solvers have experienced dramatic improvements in their performance and scalability over the last several years according to E. Goldberg et al. (2002) and are now routinely used in diverse EDA applications. Nevertheless, a number of practical SAT instances remain difficult to solve in SAT 2002 Competition (http://www.satlive.org/SATCompetition/submittedbenchs.html) and continue to defy even the best available SAT solvers according to E. Goldberg et al. (2002). Recent work pointed out that symmetries in the Boolean search space are often to blame. A theoretical framework for detecting and breaking such symmetries was introduced in J. Crawford et al. (1996). This framework was subsequently extended, refined, and empirically shown to yield significant speed-ups for a large number of benchmark classes in F. Aloul et al. (2002). Symmetries in the search space are broken by adding appropriate symmetry-breaking predicates (SBPs) to a SAT instance in conjunctive normal form (CNF). The SBPs prune the search space by acting as a filter that confines the search to nonsymmetric regions of the space without affecting the satisfiability of the CNF formula. For symmetry breaking to be effective in practice, the computational overhead of generating and manipulating the SBPs must be significantly less than the run time savings they yield due to search space pruning. In this paper, we present several new constructions of SBPs that improve on previous work. Specifically, we give a linear-sized CNF formula that selects lex-leaders (among others) for single permutations. We also show how that formula can be simplified by taking advantage of the sparsity of permutations. We test these improvements against earlier constructions and show that they yield smaller SNPs and lead to run time reductions on many benchmarks.