Talks and Poster Presentations (with Proceedings-Entry):
M. Kirchweger, S. Szeider:
"SAT Modulo Symmetries for Graph Generation";
Talk: International Conference on Principles and Practice of Constraint Programming (CP),
Montpellier, France;
2021-10-25
- 2021-10-29; in: "27th International Conference on Principles and Practice of Constraint Programming (CP 2021)",
LIPICS,
210
(2021),
ISBN: 978-3-95977-211-2;
1
- 16.
English abstract:
We propose a novel constraint-based approach to graph generation. Our approach utilizes the
interaction between a CDCL SAT solver and a special symmetry propagator where the SAT solver
runs on an encoding of the desired graph property. The symmetry propagator checks partially
generated graphs for minimality w.r.t. a lexicographic ordering during the solving process. This
approach has several advantages over a static symmetry breaking: (i) symmetries are detected early
in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure,
and (iii) the propagator can perform a complete symmetry breaking without causing a prohibitively
large initial encoding. We instantiate our approach by generating extremal graphs with certain
restrictions in terms of girth and diameter. With our approach, we could confirm the Simon-Murty
Conjecture (1979) on diameter-2-critical graphs for graphs up to 18 vertices.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.4230/LIPIcs.CP.2021.34
Electronic version of the publication:
https://publik.tuwien.ac.at/files/publik_300078.pdf
Created from the Publication Database of the Vienna University of Technology.