Faculté des Sciences appliquées
Faculté des Sciences appliquées

Modeling and Solving Problems Using Propositional Logic and SAT Solvers

Aldeghi, Florian ULiège
Promotor(s) : Fontaine, Pascal ULiège
Date of defense : 26-Jun-2023/27-Jun-2023 • Permalink :
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 ULiège
Date of defense  : 26-Jun-2023/27-Jun-2023
Advisor(s) : Fontaine, Pascal ULiège
Committee's member(s) : Boigelot, Bernard ULiège
Schindler, Tanja ULiège
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 : Student
General 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


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



Access TFE.pdf
Size: 1.18 MB
Format: Adobe PDF


Access résumé_TFE.pdf
Size: 86.43 kB
Format: Adobe PDF


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


Committee's member(s)

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

All documents available on MatheO are protected by copyright and subject to the usual rules for fair use.
The University of Liège does not guarantee the scientific quality of these students' works or the accuracy of all the information they contain.