News from the research group Knowledge Representation and Reasoning of February 14, 2016

EMCL Best Master Thesis Award 2015

Adrián Rebola-Pardo has obtained the Best Master Thesis Award of EMCL 2015 for his thesis "Unsatisfiability Proofs in SAT Solving with Parity Reasoning".

The prize is awarded with 1,000 EUR. The other two candidates were Alina Aleksandrova and Radityo Eko Prasojo.

Abstract:

SAT solvers have become very efficient in the last two decades, due to the use of many techniques. Because of the increase in code complexity, measures to increase reliability of results reported by SAT solvers were implemented. Currently, state-of-the-art SAT solvers are able to produce unsatisfiability proofs when confronted with an unsatisfiable instance. However, it is not known how to generate unsatisfiability proofs for a few very proficient techniques, and this situation forces these techniques to be disabled when unsatisfiability proofs are required.

One such technique is parity reasoning, which is essential to the application of SAT solvers to cryptography. In this talk, we solve the problem of generating unsatisfiability proofs for SAT solvers with integrated parity reasoning. In doing so, some theoretical contributions are proposed, including a generalized framework for proof systems that is able to model the DRAT proof

standard, currently used by state-of-the-art solvers.