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

Satisfiability Modulo Theories for finite domains

Dasnois, Louis ULiège
Promotor(s) : Fontaine, Pascal ULiège
Date of defense : 4-Sep-2023/5-Sep-2023 • Permalink :
Title : Satisfiability Modulo Theories for finite domains
Author : Dasnois, Louis ULiège
Date of defense  : 4-Sep-2023/5-Sep-2023
Advisor(s) : Fontaine, Pascal ULiège
Committee's member(s) : Boigelot, Bernard ULiège
Schindler, Tanja ULiège
Language : English
Discipline(s) : Engineering, computing & technology > Computer science
Institution(s) : Université de Liège, Liège, Belgique
Degree: Master : ingénieur civil en informatique, à finalité spécialisée en "computer systems security"
Faculty: Master thesis of the Faculté des Sciences appliquées


[en] This thesis investigates strategies to improve and extend modern SMT solving procedures to effectively handle problems involving finite domains, whether they are explicitly defined or concealed within the problem's encoding. The research comprises both theoretical analyses and empirical evaluations. The central contributions are twofold:

First, a quantifier elimination strategy is developed. The research reveals that quantifiers significantly hinder solver efficiency when applied to finite domains, using Sudoku as an example. An algorithm is introduced to automatically detect ``effective finite domains'' in quantified Skolem formulas over integers, and eliminate quantifiers through exhaustive instantiation. A prototype implementation is made, showing this procedure improves solver performance and can be used even with solvers lacking quantifier support.

Second, the thesis explores the theory of uninterpreted functions with domain cardinality constraints. It establishes the NP-completeness of the satisfiability problem for a set of literals in this theory. SAT-based algorithms extending classical congruence closure are proposed, ensuring the efficiency of congruence closure for large or infinite domains while transitioning to SAT solvers for smaller domains. The proposed algorithms await implementation and validation within an SMT framework. Notably, addressing the loss of conflict set generation and equality deduction when SAT is employed remains an open challenge for future research.



Access Satisfiability_Modulo_Theories_for_finite_domains.pdf
Size: 612.86 kB
Format: Adobe PDF


Access Satisfiability_Modulo_Theories_for_Finite_Domains___Summary.pdf
Size: 91.64 kB
Format: Adobe PDF


  • Dasnois, Louis 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 25

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.