CDCLSym swMATH ID: 43896 Software Authors: Metin, Hakan; Baarir, Souheib; Colange, Maximilien; Kordon, Fabrice Description: CDCLSym: introducing effective symmetry breaking in SAT solving. 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. This paper presents a new way to handle symmetries, that avoid the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. Our proposal has been implemented in MiniSym. Extensive experiments on the benchmarks of last six SAT competitions show that our approach is competitive with the best state-of-the-art static symmetry breaking solutions. .. This approach is implemented in the C++ library called cosy. Homepage: https://link.springer.com/chapter/10.1007/978-3-319-89960-2_6 Source Code: https://github.com/lip6/cosy Dependencies: C++ Keywords: Boolean satisfiability; static symmetry breaking; dynamic symmetry breaking; symmetry-based reduction Related Software: SymChaff; MiniSat; MiniSym; Saucy; bliss Cited in: 2 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year CDCLSym: introducing effective symmetry breaking in SAT solving. Zbl 1423.68462Metin, Hakan; Baarir, Souheib; Colange, Maximilien; Kordon, Fabrice 2018 all top 5 Cited by 6 Authors 1 Baarir, Souheib 1 Colange, Maximilien 1 Fujita, Tomohiro 1 Kordon, Fabrice 1 Matsuzaki, Takuya 1 Metin, Hakan Cited in 0 Serials Cited in 1 Field 2 Computer science (68-XX) Citations by Year