[Club2] Invitation: Functional Implementation of an Optimized UNSAT Proof-Che... @ Wed May 10, 2017 14:45 - 15:15 (CEST) (club2 at mailbroy.informatik.tu-muenchen.de)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Functional Implementation of an Optimized UNSAT Proof-Checker
Speaker: Maximilian Kirchmeier
Type: Bachelor's Thesis Presentation
Description:
In meiner Arbeit geht es um die funktionale Implementation  
eines "Unsatisfiability Proof"-Checkers in OCaml. Solche UNSAT-Zertifikate  
geben SAT-Solver aus, um die Unerfüllbarkeit einer CNF-Formel zu beweisen.  
Das bisher verbreitetste Format für so ein Zertifikat ist das DRAT Format  
(für Deletion-RAT; RAT = Resolution Asymmetric Tautology). Jedes von diesen  
Zertifikaten stellt selber eine Art CNF-Formel dar, wobei jede Klausel  
darin beweisbar impliziert ist durch die Menge der Klauseln "davor", also  
die Klauseln in der CNF-Formel selbst und die Klauseln des Beweises, die  
vorher aufgeführt wurden. Am Ende so eines Beweises steht dann die leere  
Klausel, die definitiv nicht erfüllbar ist. Wenn die also auch impliziert  
ist durch die vorherigen Klauseln, hat man bewiesen, dass die Formel  
unerfüllbar ist.
Die Referenzimplementierung für so einen "DRAT Proof-Checker", der eben  
genau sichergeht, dass jede Klausel im Beweis schon impliziert war, heißt  
DRAT-trim. Ich habe jetzt einen DRAT-Checker in OCaml implementiert, mit  
dem Hintergedanken, dass Peter selbst an einem verifizierten DRAT-Checker  
arbeitet und dafür erst einmal ein brauchbares funktionales "Template"  
braucht. Obwohl es ja ein ziemlich schweres Unterfangen ist, mit einer  
Sprache wie OCaml gegen ein (halbwegs) optimiertes C-Programm anzukommen,  
habe ich jedenfalls mittlerweile einen Checker, der nur noch etwa halb so  
langsam ist wie DRAT-trim... was schon ein ganz ordentliches Ergebnis ist,  
würde ich sagen.
Vorstellen werde ich dann vor allem wie man so ein DRAT-Zertifikat konkret  
überprüft und was mir so für Optimierungen eingefallen sind, um mein  
Programm schneller zu machen.
When: Wed May 10, 2017 14:45 – 15:15 Berlin
Where: MI 00.09.038 (Turing)
Calendar: club2 at mailbroy.informatik.tu-muenchen.de
Who:
     * Julian Brunner - creator
     * club2 at mailbroy.informatik.tu-muenchen.de
     * m.kirchmeier at tum.de

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=aTdqZ2FxamppNnZuaHZmMTZja2doNm1taHMgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTY0NWQzNjY2NWIwNjFmNTQ4N2ViNjE5YzVjZTk0NWRkYjY5OTk2NzI&ctz=Europe/Berlin&hl=en

Invitation from Google Calendar: https://www.google.com/calendar/

You are receiving this courtesy email at the account  
club2 at mailbroy.informatik.tu-muenchen.de because you are an attendee of  
this event.

To stop receiving future updates for this event, decline this event.  
Alternatively you can sign up for a Google account at  
https://www.google.com/calendar/ and control your notification settings for  
your entire calendar.

Forwarding this invitation could allow any recipient to modify your RSVP  
response. Learn more at  
https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20170508/dc3d30c5/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 3219 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20170508/dc3d30c5/attachment-0001.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 3280 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20170508/dc3d30c5/attachment-0001.bin>