View source for Topic Verified SAT based Decision Procedures/en

{{Abschlussarbeit
|Titel DE=Verifizierte SAT-basierte Entscheidungsprozeduren
|Titel EN=Verified SAT-based Decision Procedures
|Abschlussarbeitstyp=Bachelor, Master, Diplom, Studienarbeit
|Betreuer=Tobias Philipp
|Abschlussarbeitsstatus=Nicht mehr verfügbar
|Beschreibung EN=The satisfiability problem (SAT) is one of the most prominent problems in theoretical computer science and has many applications in software verification, planning, bioinformatics or scheduling. Satisfiability solvers have become more complex in recent years due to inprocessing techniques and parallel computing. This raises the question whether the results of these solvers can be trusted. To gain confidence in the correctness of the results, SAT solvers can emit unsatisfiability proofs that can be validated using a checker.

However, the translation from SAT-based decision procedures, such as in answer set programming, bounded model checking, etc. can also be incorrect.
Therefore, implementing such translations to SAT in a functional programming language, and afterwards proving correctness of the the translation is important.
The combination of mechanically verified translations with the certificates from SAT solvers then leads to trustful computations.
}}