From ed9deef1d040dfc74ce74f965824983c53769aa3 Mon Sep 17 00:00:00 2001 From: luigilebroccoli <noemie.catherinot@orange.fr> Date: Tue, 12 Nov 2024 23:17:15 +0100 Subject: [PATCH] Update README.md --- README.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 9edf357..0a71876 100644 --- a/README.md +++ b/README.md @@ -3,19 +3,19 @@ Ceci est notre implementation en OCaml d'un SAT Solver utilisant l'algorithme CDCL, pour le cours "Logical aspects of IA" du M1 MPRI. Voici quelques éléments qui décrivent les spécificités de notre implémentation : -+ Lors d'un conflit, notre implémentation apprend la clause minimale (en nombre de littéraux), qui ne contient que des négations de choix et qui rend fausse la clause concernée par le conflit. Autrement dit, lorsqu'une clause C devient fausse pour un certain assignement m, on considère la négation des choix l faits dans m qui ont mené à ce que des littéraux de C soit faux - que ce soit par un choix (opposé dans littéral de C), ou par unit propagation depuis une autre clause C' ; auquel cas on considère également les choix qui ont mené à unit propagate C', et on procède récursivement. Afin d'adopter ce fonctionnement, chaque clause est muni d'un identifiant unique, et chaque littéral l de l'assignement courant contient des informations supplémentaires : son décision level, ainsi qu'un entier qui vaut -1 lorsque l est un choix fait par l'algorithme, et une valeur ci (qui est l'identifiant d'une clause C) lorsque l a été fixé par unit propagation sur C*. -(*ou, alternativement, que l apparaît dans C et que -l n'apparait dans aucune autre clause) ++ Lors d'un conflit, notre implémentation apprend la clause minimale (en nombre de littéraux), qui ne contient que les négations des choix qui ont mené à ce conflit. Autrement dit, lorsqu'une clause C devient fausse pour un certain assignment m, on considère la négation des choix l faits dans m qui ont mené à ce que les littéraux de C soit faux - que ce soit par un choix (qui assign un littéral de C à false), ou par unit propagation depuis une autre clause C' ; auquel cas on considère également les choix qui ont mené à unit propagate C', et on procède récursivement. Afin d'adopter ce fonctionnement, chaque clause est munie d'un identifiant unique, et chaque littéral l de l'assignement courant contient des informations supplémentaires : le decision level au moment de son assignment, ainsi qu'un entier qui vaut -1 lorsque l est un choix fait par l'algorithme, ou une valeur ci (qui est l'identifiant d'une clause C) lorsque l a été fixé par C*. +(* à la suite d'une unit propagation ou si l apparaît dans C et que -l n'apparait dans aucune autre clause) + Incidentalement, notre schéma d'apprentissage respecte l'heuristique UIP (unique implication point) et également l'heuristique RUP (reverse unit propagation), et ce de manière minimale. -+ Ce schema d'apprentissage est précisément le schema "decision" décrit par Zhang et al. dans "Efficient conflict driven learning in a boolean satisfiability solve", L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik, 2001. ++ Ce schéma d'apprentissage est précisément le schéma "decision" décrit par Zhang et al. dans "Efficient conflict driven learning in a boolean satisfiability solve", L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik, 2001. -+ Une implémentation basique de redémarrage de l'algorithme est aussi implémentée : un "static restart" qui va vider l'assignement courant, ici, à chaque fois que le nombre de conflits observés (nombre d'appel à la fonction "backtracking") dépasse un seuil r fixé. ++ Une implémentation basique de redémarrage de l'algorithme est aussi implémentée : un "static restart" qui va vider l'assignment courant, ici, à chaque fois que le nombre de conflits observés (nombre d'appels à la fonction "backtracking") dépasse un seuil r fixé. -+ Les clauses d'origine, ainsi que celles apprises par l'algorithme, sont stockées dans une table dynamique qui reste globale. En revanche, une formule "courante" (où l'assignement partiel courant est appliqué) est manipulée par l'algorithme afin de faciliter les tests d'insatisfiabilité par l'assignement courant. Puisque reconstituer la formule et réappliquer l'assignement suite à un backtracking peut être couteux, une pile "fstack" est maintenue, qui garde en mémoire l'état de la formule avant chaque choix de littéral (i.e. pour chaque décison level) ; cette pile fstack (formula stack) est l'équivalent explicite de la pile des appels de fonctions dans l'algorithme de dpll. ++ Les clauses de la cnf d'origine, ainsi que celles apprises par l'algorithme, sont stockées dans une table dynamique globale. En revanche, une formule "courante" (où l'assignment partiel courant est appliqué) est manipulée par l'algorithme afin de faciliter les tests d'insatisfiabilité par l'assignment courant. Puisque reconstituer la formule et réappliquer l'assignment suite à un backtracking peut être coûteux, une pile "fstack" est maintenue, qui garde en mémoire l'état de la formule avant chaque choix de littéral (i.e. pour chaque décison level) ; cette pile fstack (formula stack) est l'équivalent explicite de la pile des appels de fonctions dans l'algorithme de dpll. -+ Dans le programme, la pile des assignements, ainsi que la pile fstack mentionnées ci-dessus, sont de longueur bornées par le nombre de variables, qui est fixes. Ainsi, ces piles sont représentés en mémoire par un tableau et un entier indiquant le prochain emplacement libre. Ainsi, on maintient des piles avec ajout et accès en temps constant, mais également où le dépilage - pour n'importe quel nombre d'élément - se fait en temps constant, ce qui est très utile lors du backtracking. ++ Dans le programme, la pile des assignements, ainsi que la pile fstack mentionnées ci-dessus, sont de longueur bornées par le nombre de variables, qui est fixe. Ainsi, ces piles sont représentées en mémoire par un tableau et un entier indiquant le prochain emplacement libre. Ainsi, on maintient des piles avec ajout et accès en temps constant, mais également où le dépilage - pour n'importe quel nombre d'élément - se fait en temps constant, ce qui est très utile lors du backtracking. -+ Notre code reprend la même structure que l'implémentation fournie pour DPLL - ainsi, la fonction "simplify" performe l'unit propagation sur toute les clauses, et mets à vrai tout littéral l tel que -l n'apparaît pas dans la formule. Par ailleurs, cette procédure permet de traiter les formules de Horn : si on performe unit propagation sur une formule de horn H de manière récursive et maximale, H et satisfiable si et seulement si le résultat final ne contient pas de clause vide. En traitant cette condition au début de notre fonction, on s'assure de traiter efficacement les clauses de Horn. ++ Notre code reprend la même structure que l'implémentation fournie pour DPLL - ainsi, la fonction "simplify" performe l'unit propagation sur toutes les clauses, et mets à vrai tout littéral "pur" l (tel que -l n'apparaît pas dans la formule). Par ailleurs, cette procédure permet de traiter les formules de Horn : si on performe unit propagation sur une formule de horn H de manière récursive et maximale, H et satisfiable si et seulement si le résultat final ne contient pas de clause vide. En traitant cette condition au début de notre fonction, on s'assure de traiter efficacement les clauses de Horn. -- GitLab