Puzzle Solving with Proof

dc.contributor.authorGiljegÄrd, Sofia
dc.contributor.authorWennerbeck, Johan
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.contributor.examinerAhrendt, Wolfgang
dc.contributor.supervisorMyreen, Magnus
dc.date.accessioned2021-09-10T07:32:46Z
dc.date.available2021-09-10T07:32:46Z
dc.date.issued2021sv
dc.date.submitted2020
dc.description.abstractThe 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.sv
dc.identifier.urihttps://hdl.handle.net/20.500.12380/304104
dc.language.isoengsv
dc.setspec.uppsokTechnology
dc.subjectencodingssv
dc.subjectSATsv
dc.subjectCNFsv
dc.subjectformal methodssv
dc.subjectformal verificationsv
dc.subjectinteractive theorem proversv
dc.subjectHOLsv
dc.subjectCakeMLsv
dc.subjectpuzzlessv
dc.titlePuzzle Solving with Proofsv
dc.type.degreeExamensarbete för masterexamensv
dc.type.uppsokH
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
HĂ€mtar...
Bild (thumbnail)
Namn:
CSE 21-49 Giljegard Wennerbeck.pdf
Storlek:
1.57 MB
Format:
Adobe Portable Document Format
Beskrivning:
License bundle
Visar 1 - 1 av 1
HĂ€mtar...
Bild (thumbnail)
Namn:
license.txt
Storlek:
1.51 KB
Format:
Item-specific license agreed upon to submission
Beskrivning: