On 06.12.2018 at 12:30 in S6, there is the following noon lecture:
Using SAT Solvers in Combinatorics and Geometry
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 it 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.
K. Däubel, S. Jäger, T. Mütze, and M. Scheucher. On orthogonal symmetric chain decompositions. 2018. [arXiv:1810.09847]
T. Mütze and M. Scheucher. On L-shaped Point Set Embeddings of Trees: First Non-embeddable Examples. In Proceedings of Graph Drawing 2018. [arXiv:1807.11043]
M. Scheucher. On Disjoint Holes in Point Sets. 2018. [arXiv:1807.10848]
M. Scheucher, H. Schrezenmaier, and R. Steiner. A Note On Universal Point Sets for Planar Graphs. 2018. [arXiv:1811.06482]
Webmaster: kamweb.mff.cuni.cz Modified: 19. 10. 2010