Improved static symmetry breaking for SAT

Jo Devriendt*, Bart Bogaerts, Maurice Bruynooghe, Marc Denecker

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

23 Citations (Scopus)

Abstract

An effective SAT preprocessing technique is the construction of symmetry breaking formulas: auxiliary clauses that guide a SAT solver away from needless exploration of symmetric subproblems. How-ever, during the past decade, state-of-the-art SAT solvers rarely incorporated symmetry breaking. This suggests that the reduction of the search space does not outweigh the overhead incurred by detecting symmetry and constructing symmetry breaking formulas. We investigate three methods to construct more effective symmetry breaking formulas. The first method simply improves the encoding of symmetry breaking formulas. The second detects special symmetry subgroups, for which complete symmetry breaking formulas exist. The third infers binary symmetry breaking clauses for a symmetry group as a whole rather than longer clauses for individual symmetries. We implement these methods in a symmetry breaking preprocessor, and verify their effectiveness on both hand-picked problems as well as the 2014 SAT competition benchmark set. Our experiments indicate that our symmetry breaking preprocessor improves the current state-of-the-art in static symmetry breaking for SAT and has a sufficiently low overhead to improve the performance of modern SAT solvers on hard combinatorial instances.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2016 - 19th International Conference, Proceedings
PublisherSpringer Verlag
Pages104-122
Number of pages19
Volume9710
ISBN (Print)9783319409696
DOIs
Publication statusPublished - 2016
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Theory and Applications of Satisfiability Testing - Bordeaux, France
Duration: 5 Jul 20168 Jul 2016
Conference number: 19

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9710
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

ConferenceInternational Conference on Theory and Applications of Satisfiability Testing
Abbreviated titleSAT
CountryFrance
CityBordeaux
Period05/07/201608/07/2016

Fingerprint Dive into the research topics of 'Improved static symmetry breaking for SAT'. Together they form a unique fingerprint.

  • Cite this

    Devriendt, J., Bogaerts, B., Bruynooghe, M., & Denecker, M. (2016). Improved static symmetry breaking for SAT. In Theory and Applications of Satisfiability Testing – SAT 2016 - 19th International Conference, Proceedings (Vol. 9710, pp. 104-122). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9710). Springer Verlag. https://doi.org/10.1007/978-3-319-40970-2_8