[Lrde Annonce] New Publication: "CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving"

We are happy to announce that the following article has been accepted for publication in the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), to be held in Thessaloniki, Greece, from April 14th to April 20th 2018.        "CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving"                     Hakan Metin (1), Souheib Baarir (1,2,3),                    Maximilien Colange (3), Fabrice Kordon (1) (1): Sorbonne Universités, UPMC, LIP6 CNRS UMR 7606, France (2): Université Paris Nanterre (3): LRDE, EPITA, Le Kremlin-Bicêtre, France 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. This paper presents a new way to handle symmetries, that avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase.  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. -- Maximilien Colange Assistant Professor LRDE -- EPITA (+33) 1 53 14 59 45