EMCL Best Master Thesis Award 2015
Neuigkeit aus der Forschungsgruppe Wissensverarbeitung vom 14. Februar 2016
EMCL Best Master Thesis Award 2015
Die beiden anderen Kandidaten waren Alina Aleksandrova und Radityo Eko Prasojo.
Englische Zusammenfassung seiner Arbeit:
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.
