ITEM METADATA RECORD
Title: BreakIDGlucose: On the importance of row symmetry in SAT
Authors: Devriendt, Jo ×
Bogaerts, Bart
Bruynooghe, Maurice #
Issue Date: 18-Jul-2014
Host Document: Proceedings 4th International Workshop on the Cross-Fertilization Between CSP and SAT pages:1-17
Conference: CSPSAT edition:2014 location:Vienna date:18 July 2014
Abstract: Symmetry is a topic studied by both the Satisfiability (SAT) and the Constraint Programming (CP) community. However, few attempts at transferring results between both communities have been made. This paper makes the link by investigating how symmetries from Constraint Satisfaction Problems (CSPs) transfer to symmetries of their SAT encodings. We point out that important symmetry groups studied in CP correspond to piecewise row symmetries of their SAT encoding, which -using a CP result- can be broken efficiently. We then show that the standard static symmetry breaking techniques for SAT fail to break these symmetries efficiently, and investigate how this can be mitigated. We also identify the Piecewise Row Interchangeability Detection problem, and we design a first automatic row interchangeability detection scheme for SAT. We implemented hese ideas in the BreakIDGlucose SAT solver, which detects and completely breaks interchangeable row symmetry. BreakIDGlucose’s first place in the hard combinatorial track of the 2013 SAT competition shows the potential of row symmetry exploitation.
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
BreakIDGlucose.pdf Submitted 304KbAdobe PDFView/Open

 


All items in Lirias are protected by copyright, with all rights reserved.