Enhancing Static Symmetry Breaking with Dynamic Symmetry Handling in CDCL SAT Solvers

摘要

Symmetry exploitation techniques in SAT can be classified into two main categories: static symmetry breaking and dynamic symmetry handling. It is currently recognized that the most effective approach is the static one, which proceeds by preprocessing the formula to be solved in order to add symmetry-breaking predicates (SBPs) that guarantee the preservation of equisatisfiability but not equivalence. Due to the large size of the CNF symmetry groups, only a subset of the SBPs is generated resulting in a partial symmetry breaking. It is at this level that dynamic symmetry handling can intervene to help the solver avoid as much as possible, the exploration of isomorphic symmetrical subspaces for symmetries not (entirely) broken by the static approach. However, the use of both techniques within the same solver could compromise the result. We propose in this paper in addition to an optimization of the dynamic scheme SLS, an approach that allows the two methods of symmetry exploitation to coexist within the same solver in order to increase its efficiency while preserving its correctness. This is to the best of our knowledge, the first time such an integration is envisaged within the framework of SAT solving. Experimental results conducted on hard combinatorial instances drawn from SAT competitions show that symmetrical learning can indeed improve static symmetry breaking.