On va réaliser dans ce TP un SAT-solver en deux parties :

un lexer/parser en OCaml qui affiche une formule en forme normale conjonctive (FNC) dans une syntaxe très simple ;
un solveur en C.

On reprend les définitions du chapitre Calcul propositionnel : un littéral est une variable ou la négation d'une variable, une clause est une disjonction de littéraux et une FNC est une conjonction de clauses. Le problème SAT consiste à déterminer si une formule, ici en FNC, est satisfiable.

OCaml : lexer et parser¶

Formules¶

On considère un type de formules logiques :

type formule =
      Var of string
    | Non of formule
    | Ou of formule * formule
    | Et of formule * formule

Question 1. Écrire une fonction permettant d'afficher une telle formule.

Question 2. Écrire une fonction qui renvoie la liste des variables présentes dans la formule, sans répétitions.

Question 3. Écrire une fonction qui vérifie si une formule est en forme normale conjonctive avec associativité à droite.

Note : on dira donc ici que \(A \wedge (B \wedge C)\) est en FNC mais pas \((A \wedge B) \wedge C\). De même, on demande que les clauses soient de la forme \(l_1 \vee (l_2 \vee (\dots \vee l_k))\) où les \(l_i\) sont des littéraux.

Forme normale conjonctive¶

On va représenter une formule en forme normale conjonctive sous la forme d'un int list list (la liste des clauses, chaque clause étant la liste de ses littéraux) où on considère une énumération \(v_1, \dots, v_n\) des variables et où un littéral \(v_i\) est représenté par l'entier \(i\) et un littéral \(\neg v_i\) par l'entier \(-i\).

Question 4. En considérant l'énumération des variables donnée par votre fonction précédente et en supposant que la formule est en FNC, afficher la formule sous forme textuelle dans le format :

nombredeclauses
nombredelitclause1 lit lit ... lit
...
nombredelitclausen lit lit ... lit

Par exemple, \(A \wedge (B \vee \neg C)\) dans l'énumération \(A,B,C\) deviendra :

2
1 1
2 2 -3

Remarque

C'est une version simplifiée du format DIMACS, utilisé par les SAT-solveurs réels, où chaque clause est terminée par un 0 au lieu d'être précédée de sa longueur.

Lexer¶

On va considérer une représentation infixe parenthésée des formules en utilisant /\ pour et, \/ pour ou, ~ pour non, où on ignore les espaces et sauts de ligne et où les parenthèses ( et ) servent à regrouper une sous-formule.

On définit donc le type lexeme

type lexeme =
      LNon | LOu | LEt | LLpar | LRpar
    | LVar of string

et, pour manipuler un flot de caractères dans une chaîne :

type lexbuf = {
    contenu : string;
    mutable curseur : int
}

let lexbuf_init s = { contenu = s; curseur = 0 }

let lexbuf_regard l j = l.contenu.[l.curseur + j]
let lexbuf_avance l k = l.curseur <- l.curseur + k
let lexbuf_fini l = l.curseur >= String.length l.contenu
exception FinLexbuf
let lexbuf_recup l =
    if lexbuf_fini l
    then raise FinLexbuf;
    let c = lexbuf_regard l 0 in
    lexbuf_avance l 1;
    c

exception ErreurLexicale

Question 5. Écrire une fonction lexer : string -> lexeme list qui découpe une chaîne en lexèmes. En cas d'erreur, on produira l'exception ErreurLexicale.

Parser¶

Question 6. Écrire une fonction parser : lexeme list -> formule * lexeme list qui lit une formule depuis un flot de lexèmes et renvoie les lexèmes non utilisés.

En cas d'erreur de syntaxe, on produira l'exception ErreurSyntaxique.

Pour que les formules lues soient en FNC au sens de la question 3, on lira A /\ B /\ C comme \(A \wedge (B \wedge C)\), et de même pour \/. On pourra supposer que /\ et \/ ne sont jamais mélangés sans parenthèses, comme dans l'exemple ci-dessous.

Le frontend¶

On pourra ainsi utiliser le code suivant

let main =
    let s = read_line () in
    let lex = lexer s in
    let f, q = parser lex in
    assert(q = []);
    assert(est_en_cnf f);
    affiche_cnf (cnf f)

pour lire une formule et l'afficher, où cnf calcule la représentation par un int list list et affiche_cnf réalise l'affichage de la question 4.

Dans la suite, on va écrire un programme resout et, si le programme OCaml est parser, on pourra exécuter dans le shell :

echo "A /\ (B \/ ~C) /\ (~A \/ ~B)" | ./parser | ./resout

pour enchaîner les opérations. Ici, ./parser affiche :

Question 7. Écrire des jeux de tests.

Résolution en C¶

Lecture des données¶

Question 8. Écrire un programme en C qui lit une formule en FNC depuis l'entrée standard.

On pourra la stocker sous la forme d'un int** et du nombre de clauses. Pour les clauses, on pourra utiliser une sentinelle 0 pour terminer les listes.

Résolution par retour sur trace¶

Question 9. Écrire un programme qui cherche si la formule est satisfiable par retour sur trace.

On pourra s'inspirer de l'algorithme de Quine : on affecte les variables une par une et on revient en arrière dès qu'une clause a tous ses littéraux faux.

Remarque

Les SAT-solveurs réels reposent sur l'algorithme DPLL, qui ajoute deux règles à ce retour sur trace : si une clause n'a plus qu'un littéral non affecté et aucun littéral vrai, ce littéral doit être rendu vrai (propagation unitaire) ; si une variable n'apparaît que positivement (ou que négativement) dans les clauses non encore satisfaites, on peut lui donner la valeur qui rend ces littéraux vrais (littéral pur). On pourra les ajouter pour accélérer la recherche.

Première parallélisation¶

Si la formule a \(n+p\) variables, on peut lancer \(2^n\) threads en parallèle avec chaque valuation des \(n\) premières variables pour explorer les \(2^p\) complétions de valuations sur les variables restantes.

Question 10. Implémenter cette stratégie. La charge est-elle bien répartie ?

Parallélisation dynamique¶

Question 11. Mettre en place un paradigme producteur-consommateur pour paralléliser le problème plus efficacement.