Martin Lester

"Easily encode problems in SAT With This One Simple Trick: Declarative programming in C using CBMC"

(MPI-SWS in Kooperation mit dem Fachbereich Informatik)

SAT solvers have advanced massively over the last 20 years. They have been successfully applied to a wide variety of problem domains, including software and hardware verification, timetabling/scheduling, cryptanalysis and classical planning. If you have a problem you want to solve, which has a polynomial-time verifiable solution, then rather than spending time searching for an efficient algorithm, you should seriously consider encoding it in SAT, so that a SAT solver can inefficiently search for a solution. Directly developing an encoding can be time-consuming and fiddly, even with higher-level libraries such as PySAT or constraint programming languages such as Picat. But if you are prepared to sacrifice some efficiency, you can write code to verify your solution in C and use a bounded model checker such as CBMC to translate it into SAT. In this talk, I will illustrate this paradigm with some examples. These will include a simple example of breaking a weak cryptographic cipher and a more complex example of finding the solution to a commercial text adventure game, where the game engine includes an interpreter for a scripting language.

Termin als Datei downloaden und in den Kalender importieren.