Se ha publicado un artículo de razonamiento formalizado en Coq sobre SAT titulado A formalised polynomial-time reduction from 3SAT to Clique.

Sus autor es Lennard Gäher del Programming Systems Lab en la Universidad del Sarre (en inglés, Saarland University y en alemán Universität des Saarlandes) en Saarbrücken, Alemania.

Su resumen es

We present a formalisation of the well-known problems SAT and Clique from computational complexity theory. From there, a polynomial-time reduction from 3SAT, a variant of SAT where every clause has exactyly three literals, is developed and verified. All the results are constructively formalised in the proof assistant Coq, including the polynomial running time bounds. The machine model we use is the weak call-by-value lambda calculus.

El trabajo forma parte de su Bachelor’s Thesis y está dirigido por Fabian Kunze.