EMCL Best Master Thesis Award 2015

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Neuigkeit aus der Forschungsgruppe Wissensverarbeitung vom 14. Februar 2016

EMCL Best Master Thesis Award 2015

Adrián Rebola-Pardo hat den EMCL Best Master Thesis Award 2015 für seine Arbeit "Unsatisfiability Proofs in SAT Solving with Parity Reasoning" gewonnen. Der Preis ist mit 1,000 EUR dotiert.

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.