Puzzle Solving with Proof
Typ
Examensarbete för masterexamen
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2021
Författare
Giljegård, Sofia
Wennerbeck, Johan
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
The development of SAT solvers is an ongoing research area, driven by the possibility
to use SAT solvers to solve a wide range of problems. This development has
made SAT solvers fast, and they solve increasingly more difficult problems. In order
to take advantage of this development, the encoding process to SAT is crucial
and must be correct. The purpose of this project is to implement a verified chain
of encoding functions. The encoding functions are written in and verified using
HOL4 as part of CakeML. The result is three different versatile datatypes that
can be used, together with a SAT solver, to solve problems containing Boolean
variables, natural numbers, and unordered sets. The usage of the three datatypes
is demonstrated on different logical puzzles. Using the verified SAT encoding chain
allows encodings of new problems to conjunctive normal form to be made with a
reduced number of proofs needed in the verification process. We believe that this
is the first instance of a verified SAT encoding chain in HOL4.
Beskrivning
Ämne/nyckelord
encodings , SAT , CNF , formal methods , formal verification , interactive theorem prover , HOL , CakeML , puzzles