Markus Kirchweger, Scheucher, M., & Szeider, S. (2023). SAT-Based Generation of Planar Graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). 26th International Conference on Theory and Applications of Satisfiability Testing (SAT), Alghero, Italy. Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2023.14
26th International Conference on Theory and Applications of Satisfiability Testing (SAT)
en
Event date:
4-Jul-2023 - 8-Jul-2023
-
Event place:
Alghero, Italy
-
Number of Pages:
18
-
Publisher:
Schloss-Dagstuhl - Leibniz Zentrum für Informatik
-
Peer reviewed:
Yes
-
Keywords:
dynamic symmetry breaking; Earth-Moon problem; Kuratowski's theorem; order dimension; planarity test; SAT modulo Symmetry (SMS); Schnyder's theorem; Turán's theorem; universal point set
en
Abstract:
To test a graph's planarity in SAT-based graph generation we develop SAT encodings with dynamic symmetry breaking as facilitated in the SAT modulo Symmetry (SMS) framework. We implement and compare encodings based on three planarity criteria. In particular, we consider two eager encodings utilizing order-based and universal-set-based planarity criteria, and a lazy encoding based on Kuratowski's theorem. The performance and scalability of these encodings are compared on two prominent problems from combinatorics: The computation of planar Turán numbers and the Earth-Moon problem. We further showcase the power of SMS equipped with a planarity encoding by verifying and extending several integer sequences from the Online Encyclopedia of Integer Sequences (OEIS) related to planar graph enumeration. Furthermore, we extend the SMS framework to directed graphs which might be of independent interest.
en
Project title:
Revealing and Utilizing the Hidden Structure for Solving Hard Problems in AI: ICT19-065 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) SAT-Basierende lokale Verbesserungsmethoden: P32441-N35 (FWF - Österr. Wissenschaftsfonds)
CC BY 4.0
