CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving - Archive ouverte HAL Access content directly
Conference Papers Year :

CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving

Hakan Metin
  • Function : Author
  • PersonId : 1030869
Souheib Baarir
  • Function : Author
  • PersonId : 961876
Fabrice Kordon

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 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.
Fichier principal
Vignette du fichier
10.1007-978-3-319-89960-2_6.pdf (1003.49 Ko) Télécharger le fichier
Origin : Publisher files allowed on an open archive
Loading...

Dates and versions

hal-01766948 , version 1 (14-04-2018)

Identifiers

  • HAL Id : hal-01766948 , version 1

Cite

Hakan Metin, Souheib Baarir, Maximilien Colange, Fabrice Kordon. CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving. Tools and Algorithms for the Construction and Analysis of Systems -- TACAS, Apr 2018, Tessaloniki, Greece. ⟨hal-01766948⟩
334 View
141 Download

Share

Gmail Facebook Twitter LinkedIn More