Breaking symmetries with lex implications

Michael Codish, Thorsten Ehlers, Graeme Gange, Avraham Itzhakov, Peter J. Stuckey

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

1 Citation (Scopus)


Breaking symmetries is crucial when solving hard combinatorial problems. A common way to eliminate symmetries in CP/SAT is to add symmetry breaking constraints. Ideally, symmetry breaking constraints should be complete and compact. The aim of this paper is to find compact and complete symmetry breaks applicable when solving hard combinatorial problems using CP/SAT approach. In particular: graph search problems and matrix model problems where symmetry breaks are often specified in terms of lex constraints. We show that sets of lex constraints can be expressed with only a small portion of their inner lex implications which are a particular form of Horn clauses. We exploit this fact and compute a compact encoding of the row-wise LexLeader and state of the art partial symmetry breaking constraints. We illustrate the approach for graph search problems and matrix model problems.

Original languageEnglish
Title of host publicationFunctional and Logic Programming
Subtitle of host publication14th International Symposium, FLOPS 2018 Nagoya, Japan, May 9–11, 2018 Proceedings
EditorsJohn P. Gallagher, Martin Sulzmann
Place of PublicationCham Switzerland
Number of pages16
ISBN (Electronic)978-3-319-90686-7
ISBN (Print)9783319906850
Publication statusPublished - 2018
Externally publishedYes
EventInternational Symposium on Functional and Logic Programming 2018
- Nagoya, Japan
Duration: 9 May 201811 May 2018
Conference number: 14th

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Symposium on Functional and Logic Programming 2018
Abbreviated titleFLOPS 2018
Internet address

Cite this