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