The ACO Seminar (2023–2024)

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.