Faculté des Sciences appliquées

### Modeling and Solving Problems Using Propositional Logic and SAT Solvers

##### Details
 Title : Modeling and Solving Problems Using Propositional Logic and SAT Solvers Translated title : [fr] Modélisation et résolution de problèmes à l'aide de la logique propositionnelle et des solveurs SAT Author : Aldeghi, Florian Date of defense  : 26-Jun-2023/27-Jun-2023 Advisor(s) : Fontaine, Pascal Committee's member(s) : Boigelot, Bernard  Schindler, Tanja Language : English Number of pages : 68 Keywords : [en] SAT solver[en] Boolean variables[en] clauses[en] model[en] computation time[en] satisfiability[en] efficiency[en] quantifier Discipline(s) : Engineering, computing & technology > Computer science Name of the research project : Modeling and Solving Problems Using Propositional Logic and SAT Solvers Target public : StudentGeneral public Institution(s) : Université de Liège, Liège, Belgique Degree: Master : ingénieur civil en informatique, à finalité spécialisée en "management" Faculty: Master thesis of the Faculté des Sciences appliquées

##### Abstract

[fr] 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.

TFE.pdf
Description:
Size: 1.18 MB

résumé_TFE.pdf
Description:
Size: 86.43 kB

### Author

• Aldeghi, Florian Université de Liège > Master ingé. civ. info., à fin.

### Committee's member(s)

• Boigelot, Bernard Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique
View his publications on ORBi
• Schindler, Tanja Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Systèmes et modélisation
View his publications on ORBi
• Total number of views 18