[Back]

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.

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.

http://dx.doi.org/10.4230/LIPIcs.CP.2021.34

https://publik.tuwien.ac.at/files/publik_300078.pdf