Étude des performances d’un solveur CDCL en OCaml

Le solveur SMT Alt-Ergo 

Alt-Ergo est un solveur SMT qui fut notre objet d’étude au cours de cette thèse. Il est développé au Laboratoire de Recherche en Informatique (LRI) de l’université Paris-Sud. Son développement débuta en 2006 et est maintenu depuis 2013 par l’entreprise OCamlPro en collaboration avec l’équipe VALS du LRI. Ce solveur fut développé dans le but de résoudre automatiquement des formules mathématiques issues de plates-formes de preuve de programmes. Son développement fut guidé par les besoins de la plate-forme Why/Why3 qui utilise une spécification riche via un langage polymorphe à la ML [42]. Pour gérer directement les formules issues de cette plate-forme, Alt-Ergo possède un langage natif se rapprochant de cette syntaxe polymorphe. Il possède aussi des capacités de raisonnement sur des structures de données définies par l’utilisateur, sur les énumérations et tableaux, sur des formules quantifiées et sur des opérations arithmétiques entières et réelles. En 2017, le support pour l’arithmétique des flottants a été également ajouté.

Le standard SMT-LIB 2

De nombreux solveurs SMT ont vu le jour à partir des années 2000, accompagnés d’une tentative de standardisation. Ce standard, SMT-LIB, fut proposé par Silvio Ranise et Cesare Tinelli [61] en 2003. Les buts étaient multiples : SMT-LIB devait proposer un standard pour les théories utilisées par les solveurs SMT via des descriptions rigoureuses. Il devait permettre d’avoir une unification des entrées et sorties des solveurs grâce à un nouveau langage de description pour les problèmes. Un autre but était de connecter les différents acteurs du monde de la satisfiabilité modulo théories en créant une communauté de chercheurs, développeurs et utilisateurs. Pour cela l’initiative fut accompagnée par l’idée de créer une grande bibliothèque de problèmes accessible à tous.

Étude des performances d’un solveur CDCL en OCaml

Des expérimentations préliminaires à cette thèse ont porté sur le remplacement du solveur SAT historique d’Alt-Ergo par méthode des tableaux, par un solveur SAT de référence (Minisat). Malheureusement cette expérimentation a montré de moins bons résultats qu’avec le solveur SAT historique de ce dernier. Une rapide comparaison entre deux implémentations de Minisat dans son langage de programmation C++ et une implémentation en OCaml ont permis de détecter des écarts de performances significatifs. Plusieurs questions ont été levées, mais sont restées sans réponse. Nous y répondons dans cette thèse. La première question portait sur les différences entre les deux implémentations C++ et OCaml. Bien qu’elles respectaient le même algorithme, de légères différences pouvaient faire varier les décisions et les résultats. Notre premier travail a donc porté sur l’implémentation rigoureusement exacte en terme fonctionnel du solveur de référence, les seules différences étant structurelles et non algorithmiques. Pour éviter au maximum des différences structurelles trop importantes, nous avons décidé d’utiliser les mêmes structures de données dans les deux implémentations. Les seules différences sont ainsi liées au langage de programmation utilisé. Nous avons ensuite étudié les différences de performances et essayé de trouver les raisons de celles-ci. Les travaux préliminaires soupçonnaient que les structures de données et la gestion automatique de la mémoire avaient un impact négatif sur les performances. Ce travail ainsi que nos conclusions sont très proches des travaux de Cruanes [28]. Enfin, nous comparerons le solveur SAT historique d’Alt-Ergo et l’implémentation du solveur SAT de référence sur des problèmes SAT, nous permettant ainsi d’étudier leur capacité de raisonnement booléen.

Intégration efficace d’un solveur CDCL dans un solveur SMT

Suite à ces travaux sur les performances du solveur SAT, nous avons décidé de nous pencher sur la combinaison de ce dernier au sein du solveur Alt-Ergo. Du fait que ses performances étaient semblables à celles du solveur de référence et bien meilleures que celles du solveur historique sur des problèmes purement booléens, nous avons validé le fait que les mauvaises performances de ce solveur dans Alt Ergo sur des problèmes SMT n’étaient pas dues au solveur SAT mais à son intégration avec le combinateur de théories et le moteur d’instanciation.

Dans un premier temps nous avons assisté le solveur historique d’AltErgo en le combinant au solveur CDCL performant pour le raisonnement booléen. Cela a permis d’obtenir une amélioration des résultats, nous motivant à approfondir cette problématique. Dans un second temps, nous avons formalisé et implémenté une solution pour améliorer l’intégration d’un solveur CDCL performant au sein d’Alt Ergo. Cette solution fut guidée par le fonctionnement du solveur historique. Nous avons en effet utilisé le fonctionnement de la méthode des tableaux pour réduire le modèle booléen transmis aux théories et au moteur d’instanciation. Cette méthode se rapproche de la technique de pertinence [33] utilisée par le solveur Z3 [32]. Plusieurs optimisations d’implémentation nous ont permis d’obtenir une solution efficace et performante que nous avons testée et comparée. Nous avons testé l’intérêt de notre optimisation sur les différentes parties d’un solveur SMT. Nous avons ainsi testé l’impact d’une telle méthode sur la combinaison de théories ainsi que sur le moteur d’instanciation.

Extension du standard SMT-LIB 2 avec du polymorphisme

Le manque de support du standard SMT-LIB 2 par Alt-Ergo nous empêche d’avoir accès à la communauté SMT et à sa base de fichiers de test. De plus, cela nous contraint pour comparer justement notre solveur aux solveurs de l’état de l’art sur des fichiers d’entrées identiques. Nous avons décidé d’ajouter le support du langage de la SMT-LIB 2 à Alt-Ergo. Le polymorphisme faisant partie intégrante du langage natif de notre solveur, nous avons souhaité modifier le standard pour y ajouter une extension polymorphe. Des travaux [16] ont d’ailleurs déjà tenté d’ajouter un support pour le polymorphisme dans SMT-LIB 2. Malheureusement ces travaux ne se focalisent que sur l’analyse lexicale et syntaxique du polymorphisme. Contrairement à ces travaux et grâce au support natif du polymorphisme par Alt-Ergo dans son moteur de raisonnement, nous souhaitons montrer l’avantage de traiter nativement le polymorphisme dans un solveur SMT.

Durant cette thèse, nous avons développé une bibliothèque permettant d’effectuer l’analyse lexicale et syntaxique du standard de la SMT-LIB 2 avec une extension polymorphe conservative et non intrusive. Alt-Ergo utilise cette bibliothèque pour supporter le standard. Grâce à l’outil Why3 nous avons pu générer un ensemble de bancs de test sous différents formats. Cela nous a permis de mettre en évidence l’importance du support natif du polymorphisme par rapport à la monomorphisation. Nous avons aussi pu comparer Alt-Ergo aux autres solveurs de la communauté sur des problèmes d’entrée strictement identiques.

Participation à la compétition SMT-COMP

L’ajout du support pour le standard SMT-LIB 2 nous a aussi permis de lancer Alt-Ergo sur les bancs de test de la communauté. Des résultats prometteurs sur certains de ces bancs de test nous ont motivés à nous lancer dans la compétition SMT de 2018. En préparation pour la participation à la compétition, nous avons apporté quelques modifications à Alt-Ergo pour obtenir de meilleurs résultats. Des efforts au sujet de l’instanciation ont été effectués, en particulier concernant les calculs des déclencheurs. Nous avons aussi effectué des expérimentations quant aux heuristiques d’Alt-Ergo pour obtenir un jeu d’option optimal. Le hardware de la compétition nous permettant d’utiliser jusqu’à quatre coeurs par problème, nous avons ajouté une option permettant de lancer plusieurs instances d’Alt-Ergo avec des options différentes. Cette parallélisation nous a permis d’optimiser les temps d’exécution par rapport à une exécution séquentielle du jeu d’option optimal. Ces optimisations nous ont permis d’améliorer nos résultats préliminaires et ont permis à Alt-Ergo de sortir de cette participation à la SMT-COMP 2018 comme un solveur SMT performant et concurrentiel.

Table des matières

1 Introduction
1 Satisfiabilité booléenne
1.1 Résolution et exploration
1.2 Méthode des tableaux analytiques
2 Satisfiabilité Modulo Théories
2.1 Le solveur SMT Alt-Ergo
2.2 Le standard SMT-LIB 2
3 Contributions de la thèse
3.1 Étude des performances d’un solveur CDCL en OCaml
3.2 Intégration efficace d’un solveur CDCL dans un solveur SMT
3.3 Extension du standard SMT-LIB 2 avec du polymorphisme
3.4 Participation à la compétition SMT-COMP
4 Plan de la thèse
2 Le solveur Alt-Ergo
1 Architecture
1.1 Gestion paresseuse de la CNF
1.2 Solveur SAT historique d’Alt-Ergo
1.3 Gestion des théories et des termes quantifiés dans AltErgo
2 Le langage natif d’Alt-Ergo
I SAT et SMT solveur
3 Vers un solveur SAT efficace en OCaml
1 Méthodologie de comparaison
1.1 Trace de décision
1.2 Consommation spatiale et temporelle
1.3 Paramètres
2 Résultats expérimentaux
2.1 Impact du langage OCaml sur les performances
2.2 Pistes d’optimisation
2.3 SatML vs solveur historique d’Alt-Ergo
3 Conclusion
4 Intégration efficace d’un solveur CDCL dans Alt-Ergo
1 Première approche : assister le solveur historique d’Alt-Ergo
avec un solveur CDCL
2 CDCL(λ(T)) : CDCL modulo Tableau(T)
2.1 Réduction du modèle booléen par méthode des Tableaux
2.2 Formalisme
2.3 Terminaison, Correction, Complétude
3 Implémentation
3.1 Calcul paresseux de la pertinence
3.2 Calcul de pertinence par frontière
3.3 Gestion du modèle pour l’instanciation
4 Résultats expérimentaux
4.1 Comparaison des différents solveurs SAT
4.2 Impact du calcul de pertinence des littéraux
5 Conclusion
II SMT-LIB et SMT-COMP
5 Extension du standard SMT-LIB2 avec du polymorphisme
1 Extension polymorphe
1.1 Syntaxe
1.2 Typage
2 Implémentation
2.1 Création d’une bibliothèque “frontend” pour le langage
2.2 Intégration à Alt-Ergo
3 Résultats expérimentaux
3.1 Génération de bancs de tests avec l’outil Why3
3.2 Impact du polymorphisme
3.3 Alt-Ergo et les autres solveurs SMT
3.4 Conclusion
6 Participation à la compétition SMT-COMP
1 SMT-COMP
1.1 Les théories et logiques de la SMT-LIB 2
1.2 Bancs de tests de la communauté SMT
1.3 Règles de la compétition
2 Préparation pour la compétition
2.1 Amélioration des heuristiques
2.2 Implémentation d’une version distribuée d’Alt-Ergo
3 Résultats
4 Conclusion
7 Conclusion

Télécharger le rapport complet