Please use this identifier to cite or link to this item:
Title: Logic for fun : solving puzzles with SAT solvers
Authors: Foo, Zhong Xian
Keywords: DRNTU::Engineering::Computer science and engineering::Computing methodologies::Symbolic and algebraic manipulation
Issue Date: 2016
Abstract: Over the years, SAT solvers have become more and more powerful; able to solve Boolean formulas with huge amounts of literals and clauses, and have seen more applications in recent technology. Decision puzzles, puzzles where one move affects subsequent moves, usually take a long time to solve using typical depth first search algorithms, while SAT solvers can solve it relatively quickly. With the prevalence of mobile phones, there are many mobile game applications that have such puzzles. However, despite their speed in solving such puzzles, SAT solvers have yet to see much use in mobile applications, in part due to the steep learning curve, lack of samples, and the need to translate First-Order-Logic (FOL) to Conjunctive-Normal-Form (CNF). To address these issues, the project is divided into 2 phases. First, code samples for Android applications making use of a popular SAT solver (MiniSat) have been made to ease the learning curve and to let developers have a point of reference for implementing a SAT solver in their mobile application. On top of that, a script has been developed to allow developers to easily translate FOL to CNF, to lower the entrance requirements for developers to start integrating SAT solvers in their applications. In this report, both phases of the project will be discussed, the breakdown of both the Android application as well as the script, alongside possible future improvements will be presented.
Rights: Nanyang Technological University
Fulltext Permission: restricted
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Student Reports (FYP/IA/PA/PI)

Files in This Item:
File Description SizeFormat 
Amended FYP Report.pdf
  Restricted Access
FYP Report (Appendix Included)1.23 MBAdobe PDFView/Open

Page view(s) 50

Updated on Jun 21, 2021

Download(s) 50

Updated on Jun 21, 2021

Google ScholarTM


Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.