Publications/metin.18.tacas

Authors

Hakan Metin, Souheib Baarir, Maximilien Colange, Fabrice Kordon

Where

Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)

Place

Thessaloniki, Greece

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2018-01-05

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.

Documents

• Paper

Bibtex (lrde.bib)

@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.},
  doi		= {10.1007/978-3-319-89960-2_6}
}