Modeling and Solving Problems Using Propositional Logic and SAT Solvers

Abstract

This research focuses on problem-solving using logical models, aiming to efficiently solve a variety of well-known puzzles and games that are known for their challenging nature. The goal is to find ways to model the problem and formulate constraints in order to reduce the computation time required to find a solution. The study expands beyond single-player puzzles and also explores two-player games. By analyzing and proposing novel solutions for different puzzle scenarios, this research explores a part of propositional logic applied to the resolution of games and puzzles. Specifically, the study explores the application of logical model to the Snake Cube puzzle, demonstrating its effectiveness. Furthermore, the efforts have enabled addressing larger puzzle instances (4x4x4 snake cube) by exploiting the symmetry properties of the problem. Additionally, the research investigates different approaches to solving the 2x2 Rubik’s Cube, with the objective of achieving reasonable solution times for the 3x3 Rubik’s Cube. This work experiment problem-solving techniques within the domain of logic-based models and lay the foundation for further improvements and applications. An analysis of the rules and scenarios of the game of Othello has been conducted to propose a model that allows the simulation of a game’s progression. Othello is a strategic game that necessitates careful planning and decision-making. The research findings revealed the minimum number of moves required to reach the end of a game for different board size, which is nine for boards of size 5 to 8. An extension of the model using quantified Boolean formulae provides a straight path towards solving the game. While the game has already been solved for a 6x6 board, the model presented here serves as a scalable foundation. With improvements in writing constraints in future research, the finale objective is to solve the full-scale 8x8 game.