Composing symmetry propagation and effective symmetry breaking for SAT solving

Abstract

SAT solving is an active research area aiming at finding solutions to a large variety of problems. Propositional Satisfiability problems often exhibit symmetry properties, and exploiting them extends the class of problems that state-of-the-art solvers can handle. Two classes of approaches have been developed to take benefit of these symmetries: Static and Dynamic Symmetry Breaking based approaches. They bring benefits for complementary classes of problems. However, and to the best of our knowledge, no tentative has been made to combine them. In this paper, we study the theoretical and practical aspects of the composition of two of these approaches, namely Symmetry Propagation and Effective Symmetry Breaking. Extensive experiments conducted on symmetric problems extracted from the last seven editions of the SAT contest show the effectiveness of such a composition on many symmetrical problems.