CDCLSym: Introducing effective symmetry breaking in SAT solving
In Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS’18)
Abstract SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones.