Скачать или смотреть Marijn Heule: Formal Methods and the Chromatic Number of the Plane

A talk from the Formal Methods in Mathematics workshop in Pittsburgh, January 2020:
http://www.andrew.cmu.edu/user/avigad...

Speaker: Marijn Heule
Title: Formal Methods and the Chromatic Number of the Plane
Slides: http://www.andrew.cmu.edu/user/avigad...
Abstract:
Today’s satisfiability solvers can not only determine whether a propositional formula can be satisfied, but they can also produce a certificate in case no satisfying assignments exists. These certificates, known as proofs of unsatisfiability, can be used for multiple purposes ranging from checking the correctness of the unsatisfiability claim to computing interpolants. In this talk, we focus on another application of proofs of unsatisfiability: computing an unsatisfiable core of the formula. The size of proofs tends to correlate to the size the corresponding unsatisfiable cores: the smaller the proof, the smaller the unsatisfiable core. We present a method to exploit this relation by computing a smaller and smaller proof of unsatisfiability to compute a small unsatisfiable core. We apply this method to improve the upper bound of the smallest unit-distance graph with chromatic number 5, which is currently a Polymath project. The method was crucial to obtain the best known bound of 510 vertices.