Improved static symmetry breaking for SAT

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu



  • KU Leuven


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.


OtsikkoTheory and Applications of Satisfiability Testing – SAT 2016 - 19th International Conference, Proceedings
TilaJulkaistu - 2016
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on Theory and Applications of Satisfiability Testing - Bordeaux, Ranska
Kesto: 5 heinäkuuta 20168 heinäkuuta 2016
Konferenssinumero: 19


NimiLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (painettu)03029743
ISSN (elektroninen)16113349


ConferenceInternational Conference on Theory and Applications of Satisfiability Testing

ID: 6631721