Combinatorics Seminar

16:00-18:00

Speaker: Manfred Scheucher

Title: Using SAT Solvers in Combinatorics and Geometry

Abstract: In this talk, we discuss how modern SAT solvers such as Minisat or
Glucose can be used to tackle mathematical problems. We present some of
our recent results on various problems to give the audience a better
understanding, which problems might be tackled in this fashion, and
which problems might not.

Besides the naive SAT formulation also further ideas might be required
to tackle certain problems -- additional constraints (such as statements
which hold "without loss of generality") might need to be added to the
SAT model so that is becomes solvable in reasonable time. In particular,
to tackle universal point sets for planar graphs, we present a
sophisticated approach which combines the following four powerful tools:
complete enumeration of order types, complete enumeration of (planar)
graphs, SAT solvers, and IP solvers.

Literature:
* K. Däubel, S. Jäger, T. Mütze, and M. Scheucher. On orthogonal
symmetric chain decompositions. To appear in Proc. EUROCOMB 2019.
[arXiv:1810.09847]
* T. Mütze and M. Scheucher. On L-shaped Point Set Embeddings of Trees:
First Non-embeddable Examples. Proc. Graph Drawing 2018. [arXiv:1807.11043]
* M. Scheucher. On Disjoint Holes in Point Sets. To appear in Proc.
EUROCOMB 2019. [arXiv:1807.10848]
* M. Scheucher, H. Schrezenmaier, and R. Steiner. A Note On Universal
Point Sets for Planar Graphs. [arXiv:1811.06482]