Reseña: Verifying refutations with extended resolution
Se ha publicado un artículo de verificación formal con ACL2 sobre sistemas SAT titulado Verifying refutations with extended resolution.
Sus autores son Marijn J. H. Heule, Warren A. Hunt, Jr. y Nathan Wetzler (de la Universidad de Tejas en Austin).
El trabajo se presentó la semana pasada en el CADE-24 (the 24th International Conference on Automated Deduction).
Su resumen es
Modern SAT solvers use preprocessing and inprocessing techniques that are not solely based on resolution; existing unsatisfiability proof formats do not support SAT solvers using such techniques. We present a new proof format for checking unsatisfiability proofs produced by SAT solvers that use techniques such as extended resolution and blocked clause addition. Our new format was designed with three goals: proofs should be easy to generate, proofs should be compact, and validating proofs must be simple. We show how existing preprocessors and solvers can be modified to generate proofs in our new format. Additionally, we implemented a mechanically-verified proof checker in ACL2 and a proof checker in C for the proposed format.
El correspondiente código ACL2 se encuentra aquí.