Valentin Montmirail

SAT solvers are efficient enough to deal with real-world applications and are able to deal with instances of hundreds of millions of variables and clauses. They are also able to prove the unsatisfiability of a formula. Because SAT solvers are becoming more and more efficient, the size of the proofs generated are becoming bigger and bigger. One recent example in 2016 by Heule et al. was famously described in the media under the name “largest mathematical proof ever” due to its size of 200 terabytes of data. Just by having a look at the proof, it is without a doubt that the explanation of why this problem has no solution is far out of human-understanding. In this talk, I will present how to make the SAT proofs as human-understandable as possible. I will explain how we can extract high-level constraints from a refutation proof by detecting structures in a hypergraph representing the lemmas. For this purpose, we generalized the well known Bron & Kerbosh algorithm to hypergraphs. Then, by using post-processing techniques on the detected constraints, we demonstrate how we can obtain a rather short and understandable proof. Afterward, we experimentally demonstrate our approach to famous sets of benchmarks and discuss the explainability. Finally, I will conclude and provide some perspectives.