License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.14
URN: urn:nbn:de:0030-drops-184767
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18476/
Kirchweger, Markus ;
Scheucher, Manfred ;
Szeider, Stefan
SAT-Based Generation of Planar Graphs
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.
BibTeX - Entry
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.14,
author = {Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
title = {{SAT-Based Generation of Planar Graphs}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18476},
URN = {urn:nbn:de:0030-drops-184767},
doi = {10.4230/LIPIcs.SAT.2023.14},
annote = {Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, planarity test, universal point set, order dimension, Schnyder’s theorem, Kuratowski’s theorem, Tur\'{a}n’s theorem, Earth-Moon problem}
}
