European Master's Program in Computational Logic

Search:
26 November 2015

Master Thesis Defence by Mr Adrian Rebola Pardo

Mr Adrian Rebola Pardo defended his master thesis on ' Unsatisfiability Proofs in SAT Solving with Parity Reasoning'


Mr Adrian Rebola Pardo defended his master thesis on ' Unsatisfiability Proofs in SAT Solving with Parity Reasoning' at TUD on 14 October 2015.

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.