Manfred Scheucher

SODA Conference 2024 Conference Paper

Flip Graph Connectivity for Arrangements of Pseudolines and Pseudocircles

• Yan Alves Radtke
• Stefan Felsner
• Johannes Obenaus
• Sandro Roch
• Manfred Scheucher
• Birgit Vogtenhuber

SAT Conference 2023 Conference Paper

SAT-Based Generation of Planar Graphs

• Markus Kirchweger
• Manfred Scheucher
• Stefan Szeider

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.

SAT Conference 2022 Conference Paper

A SAT Attack on Rota's Basis Conjecture

• Markus Kirchweger
• Manfred Scheucher
• Stefan Szeider

The SAT modulo Symmetries (SMS) is a recently introduced framework for dynamic symmetry breaking in SAT instances. It combines a CDCL SAT solver with an external lexicographic minimality checking algorithm. We extend SMS from graphs to matroids and use it to progress on Rota’s Basis Conjecture (1989), which states that one can always decompose a collection of r disjoint bases of a rank r matroid into r disjoint rainbow bases. Through SMS, we establish that the conjecture holds for all matroids of rank 4 and certain special cases of matroids of rank 5. Furthermore, we extend SMS with the facility to produce DRAT proofs. External tools can then be used to verify the validity of additional axioms produced by the lexicographic minimality check. As a byproduct, we have utilized our framework to enumerate matroids modulo isomorphism and to support the investigation of various other problems on matroids.