@InProceedings{   metin.18.tacas,
  author        = {Hakan Metin and Souheib Baarir and Maximilien Colange and
                  Fabrice Kordon},
  title         = {CDCLSym: Introducing Effective Symmetry Breaking in SAT
                  Solving},
  booktitle     = {Proceedings of the 24th International Conference on Tools
                  and Algorithms for the Construction and Analysis of Systems
                  (TACAS'18)},
  year          = 2018,
  month         = apr,
  pages         = {99--114},
  publisher     = {Springer},
  series        = {Lecture Notes in Computer Science},
  volume        = 10805,
  address       = {Thessaloniki, Greece},
  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.},
}