Session I.3 - Graph Theory and Combinatorics - Semi-plenary talk
Wednesday, June 14, 16:30 ~ 17:30
A SAT Approach to the Hadwiger-Nelson Problem
Marijn Heule
Carnegie Mellon University, United States - This email address is being protected from spambots. You need JavaScript enabled to view it.
Progress in satisfiability (SAT) solving has made it possible to answer long-standing open questions in mathematics. In this talk, we apply SAT techniques to the Hadwiger-Nelson problem, also known as the chromatic number of the plane. We will highlight the effectiveness of SAT to reduce the size of unit-distance graphs while preserving the chromatic number. The presented techniques were able to produce a 5-chromatic unit-distance graph with 510 vertices, which is the smallest certificate for the current lower bound of the Hadwiger-Nelson problem. We will also present a SAT-based approach to improve upper-bound results on unit-distance strips. Finally, we will discuss the challenges to increasing the lower bound of the chromatic number of the plane to 6 using automated reasoning.