Feedback

Faculté des Sciences appliquées
Faculté des Sciences appliquées
MASTER THESIS
VIEW 20 | DOWNLOAD 44

Chronological vs. non-chronological backtracking in satisfiability modulo theories

Download
Coutelier, Robin ULiège
Promotor(s) : Fontaine, Pascal ULiège
Date of defense : 4-Sep-2023/5-Sep-2023 • Permalink : http://hdl.handle.net/2268.2/18041
Details
Title : Chronological vs. non-chronological backtracking in satisfiability modulo theories
Translated title : [fr] Retour chornologique vs. non-chronologique pour la satisfaisabilité modulo théorie.
Author : Coutelier, Robin 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
Number of pages : 76
Keywords : [en] SAT
[en] SMT
[en] Chronological Backtracking
[en] Logic
Discipline(s) : Engineering, computing & technology > Computer science
Institution(s) : Université de Liège, Liège, Belgique
Degree: Master en ingénieur civil en informatique, à finalité spécialisée en "intelligent systems"
Faculty: Master thesis of the Faculté des Sciences appliquées

Abstract

[en] SMT solvers are a powerful tool used in many verification applications. They are designed to check the satisfiability of a logic formula in a given set of theories. The core of any SMT solvers is a fine-tuned SAT solver enhanced with more expressive theory reasoners. Recently, SAT solvers have seen a new paradigm emerge with the introduction of Chronological Backtracking. This new approach has already shown some improvements on state-of-the-art standalone SAT solvers. In the following, we detail the functioning of CDCL solvers and the assumptions that non-chronological backtracking enables. After that, we study what it takes to convert a standard SAT solver to support chronological backtracking. We discuss both necessary and optional changes to the solver and present algorithms for each of them. We implement these changes on the SAT solver of veriT, an SMT solver written in C. Finally, we consider some details when adapting the SMT solver to support chronological backtracking. We present ideas for future work and discuss the potential benefits of this new approach.


File(s)

Document(s)

File
Access Chronological_vs_Non-Chronological_Backtracking_in_SMT.pdf
Description:
Size: 779 kB
Format: Adobe PDF

Author

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

Promotor(s)

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 20
  • Total number of downloads 44










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.