Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry

摘要

Research in algorithms for Boolean satisfiability (SAT) and their implementations has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks can now be solved in seconds on commodity PCs. More recent benchmarks take longer to solve due of their large size, but are still solved in minutes. Yet, small and difficult SAT instances must exist if P not equal NP. To this end, our work articulates SAT instances that are unusually difficult for their size, including satisfiable instances derived from Very Large Scale Integration (VLSI) routing problems. With an efficient implementation to solve the graph automorphism problem, we show that in structured SAT instances difficulty may be associated with large numbers of symmetries. We point out that a previously published symmetry- detection mechanism based on a reduction to the graph automorphism problem often produces many spurious symmetries. Our work contributes two new reductions to graph automorphism, which detect all correct symmetries detected previously as well as phase-shift symmetries not detected earlier. The correctness of our reductions is rigorously proven, and they are evaluated empirically. We also formulate an improved construction of symmetry-breaking clauses in terms of permutation cycles and propose to use only generators of symmetries in this process. These ideas are implemented in a fully automated flow that first detects symmetries in a given SAT instance, pre-processes it by adding symmetry-breaking clauses and then calls a state-of-the-art backtrack SAT solver. Significant speed-ups are shown on many benchmarks versus direct application of the solver. In an attempt to further improve the practicality of our approach, we propose a scheme for fast opportunistic symmetry detection and also show that considerations of symmetry may lead to more efficient reductions to SAT in the VLSI routing domain.