Logic for fun : solving puzzles with SAT solvers

• Main Author: Foo, Zhong Xian
• Other Authors: Alwen Fernanto Tiu
• Format: Final Year Project
• Language: English
• Published: 2016
• Subjects: DRNTU::Engineering::Computer science and engineering::Computing methodologies::Symbolic and algebraic manipulation
• Online Access: http://hdl.handle.net/10356/66900
• Institution: Nanyang Technological University

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.