CosySEL: Improving SAT Solving Using Local Symmetries

Authors

S Saouli, S Baarir, C Dutheillet, J Devriendt

Where

24th International Conference on Verification, Model Checking, and Abstract Interpretation

Place

Boston, USA

Type

inproceedings

Projects

AA"AA" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.

Date

2022-12-08

Abstract

Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them. In this paper, we present a new toolCosySEL, that implements a composition of the static Effective Symmetry Breaking Predicates (esbp) technique with the dynamic Symmetric Explanation Learning (sel). esbp exploits symmetries to prune the search tree and sel uses symmetries to speed up the tree traversal. These two accelerations are complementary and their combination was made possible by the introduction of Local symmetries. We conduct our experiments on instances issued from the last ten sat competitions and the results show that our tool outperforms the existing tools on highly symmetrical problems

Bibtex (lrde.bib)

@InProceedings{	  saouli.23.vmcai,
  author	= {S. Saouli and S. Baarir and C. Dutheillet and J.
		  Devriendt},
  title		= {CosySEL: Improving SAT Solving Using Local Symmetries},
  booktitle	= {24th International Conference on Verification, Model
		  Checking, and Abstract Interpretation},
  year		= 2023,
  address	= {Boston, USA},
  month		= jan,
  abstract	= { Many satisfiability problems exhibit symmetry properties.
		  Thus, the development of symmetry exploitation techniques
		  seems a natural way to try to improve the efficiency of
		  solvers by preventing them from exploring isomorphic parts
		  of the search space. These techniques can be classified
		  into two categories: dynamic and static symmetry breaking.
		  Static approaches have often appeared to be more effective
		  than dynamic ones. But although these approaches can be
		  considered as complementary, very few works have tried to
		  combine them. In this paper, we present a new tool,
		  CosySEL, that implements a composition of the static
		  Effective Symmetry Breaking Predicates (esbp) technique
		  with the dynamic Symmetric Explanation Learning (sel). esbp
		  exploits symmetries to prune the search tree and sel uses
		  symmetries to speed up the tree traversal. These two
		  accelerations are complementary and their combination was
		  made possible by the introduction of Local symmetries. We
		  conduct our experiments on instances issued from the last
		  ten sat competitions and the results show that our tool
		  outperforms the existing tools on highly symmetrical
		  problems },
  note		= {accepted}
}