Improved static symmetry breaking for SAT

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

Researchers

Research units

  • KU Leuven

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.

Details

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2016 - 19th International Conference, Proceedings
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

ID: 6631721