Puzzle Solving with Proof

Typ
Examensarbete för masterexamen
Program
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
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material
Index