Puzzle Solving with Proof

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/304104
Download file(s):
File Description SizeFormat 
CSE 21-49 Giljegard Wennerbeck.pdf1.6 MBAdobe PDFView/Open
Bibliographical item details
Type: Examensarbete för masterexamen
Title: Puzzle Solving with Proof
Authors: Giljegård, Sofia
Wennerbeck, Johan
Abstract: 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.
Keywords: encodings;SAT;CNF;formal methods;formal verification;interactive theorem prover;HOL;CakeML;puzzles
Issue Date: 2021
Publisher: Chalmers tekniska högskola / Institutionen för data och informationsteknik
URI: https://hdl.handle.net/20.500.12380/304104
Collection:Examensarbeten för masterexamen // Master Theses

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.