News23: Unterschied zwischen den Versionen
Tobias Philipp (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=EMCL Best Master Thesis Award 2015 |Titel EN=EMCL Best Master Thesis Award 2015 |Beschreibung DE=Adrián Rebola-Pardo hat den EMCL Best M…“) |
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 22: | Zeile 22: | ||
a generalized framework for proof systems that is able to model the DRAT proof | a generalized framework for proof systems that is able to model the DRAT proof | ||
standard, currently used by state-of-the-art solvers. | standard, currently used by state-of-the-art solvers. | ||
|Beschreibung EN=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". | |Beschreibung EN=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 prize is awarded with 1,000 EUR. | ||
| Zeile 44: | Zeile 43: | ||
a generalized framework for proof systems that is able to model the DRAT proof | a generalized framework for proof systems that is able to model the DRAT proof | ||
standard, currently used by state-of-the-art solvers. | standard, currently used by state-of-the-art solvers. | ||
|Datum=2016/02/14 | |Datum=2016/02/14 | ||
|Forschungsgruppe=Wissensverarbeitung | |Forschungsgruppe=Wissensverarbeitung | ||
}} | }} | ||
Aktuelle Version vom 14. Februar 2016, 22:41 Uhr
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.
