INFO501 : logique (et informatique)

TP 2 : SAT solveur

Automne 2020

• Consignes

  • Outils nécessaires, prérequis

    • Debian / Ubuntu

    • macOS

  • Point important

• Liens utiles

• Préliminaires

  • Rappels : le problème

  • La structure de données utilisée : variables, littéraux et clauses

  • L'algorithme naïf

    • Les solutions partielles

    • Le code

    • Invariants et assertions

• 1. Amélioration de la structure de données : "watch lists"

  • Profilage

    • Utilisation de gprof

    • Utilisation de callgrind

  • 1.1. "Watch lists"

    • Exemples très simples

    • Benchmarks

  • 1.2. Liste des variables actives

• 2. Algorithme DPLL, avec "watch lists" et variables actives

  • 2.1. Recherche des clauses unitaires

  • 2.2. Quelques tests

Consignes

Outils nécessaires, prérequis

Pour ce TP, vous devez disposer d'un environnement de type Unix avec

• un compilateur C (gcc ou clang),

• la commande make,

• la commande gprof et/ou l'outil valgrind,

• le programme minisat pour tester et comparer notre solveur avec un solveur performant (dernière question).

Debian / Ubuntu

Les paquets suivants devraient être suffisants et sont probablement déjà installés (à part minisat) :

$ sudo apt install gcc make minisat

Vous pouvez ajouter quelques autres paquets, mais ce n'est pas obligatoire.

$ sudo apt install clang valgrind kcachegrind

macOS

Pour les étudiants qui veulent faire leur TP sous macOS, il est impératif que vous installiez ces outils avant la séance :

• clang

• make

• valgrind

• minisat (s'il n'est pas disponible dans les paquets officiels, vous pouvez le compiler directement : https://github.com/niklasso/minisat)

Point important

Liens utiles

• code à compléter : TP2-info501.tgz

• la pages des codes de D. Knuth qui a écrit un petit livre sur les SAT solveur. Nous allons essentiellement faire les versions SAT0W et SAT10

• la page Wikipedia sur l'algorithme DPLL

• la page de minisat, un petit SAT solveur écrit en C++ qui fait du "conflict-driven clause learning". Ce programme est disponible sous Debian / Ubuntu.

Préliminaires

L'objectif de ce TP est de regarder comment les SAT solveurs sont écrits. La version utilisée dans le TP1 permet de comprendre le principe théorique, mais l'efficacité n'était pas trop au rendez vous !

Nous allons donc coder un SAT solveur (du style DPLL), en C, en utilisant des structures de données adaptées.

Rappels : le problème

Étant donnée une formule en forme normale conjonctive (FNC), comme (x₁ ∨ ¬x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃ ∨ x₄) ∧ (x₂ ∨ ¬x₄) le solveur doit chercher des valeurs pour x₁, ..., x₄ qui rendent la formule vraie.

La méthode standard utilise le backtracking : on essaie des solutions, et quand elles ne conviennent pas, on modifie la dernière décision possible.

La version naïve du TP1 était récursive, mais pour gagner en performances, nous allons devoir passer à une version itérative.

La structure de données utilisée : variables, littéraux et clauses

Chaque formule en FNC, comme (x₁ ∨ ¬x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃ ∨ x₄) ∧ (x₂ ∨ ¬x₄) sera représentée par 2 tableaux :

1. Lit, qui donne la liste de tous les littéraux apparaissant dans la formule. (Il y a par exemple 8 littéraux dans la formule ci dessus.)

   Chaque littéral sera représenté par un entier :

   • 2k+1 pour le littéral x_k

   • 2k pour le littéral ¬x_k

   Il n'y a pas de variable x₀. Les littéraux commencent donc à 2.

   On peut récupérer :

   • le "signe" d'un littéral en prenant son bit de poids faible : lit & 1 (macro SIGN(lit) dans le code fourni)

   • la "variable" d'un littéral en faisant un décalage de bits : lit >> 1 (macro VARIABLE(lit) dans le code fourni)

   Pour la formule ci dessus, le tableau ressemblerait à

   	clause 0			clause 1			clause 2
   littéral	x1	¬x2	x3	¬x1	¬x3	x4	x2	¬x4
   i	0	1	2	3	4	5	6	7
   Lit[i]	3	4	7	2	6	9	5	8

2. Cl, qui donne pour chaque clause (0, 1 et 2 ci dessus), l'indice du premier littéral de la clause. Ici, on aurait

   k	0	1	2	3
   Cl[k]	0	3	6	8

   Notez que le tableau Cl contient une case supplémentaire pour savoir où se termine la dernière clause : la clause k contient les littéraux de Cl[k] jusqu'à Cl[k+1]-1 (inclus).

Ces deux tableaux, avec le nombre de variables, clauses et littéraux sont stockés dans une structure :

typedef struct {
    int nb_var;     // number of different variables x_1, ..., x_n
    int nb_cl;      // number of clauses in the CNF formula
    int nb_lit;     // total number of literals in the CNF formula
    int* Lit;       // array of literals (of size nb_lit)
    int* Cl;        // array of size nb_cl+1 giving the start of each clause in the Lit array
} formula_t;

Vous pouvez appeler la fonction de tests (que vous pourrez compléter au fur et à mesure du TP) du fichier test-NOM.c. Par exemple, le test struct permet d'afficher le contenu de la structure correspondant à la formule lue dans le fichier correspondant :

$ ./sat -T struct CNF-files/test-001.cnf
The formula contains 4 variable(s), 3 clause(s) for a total of 8 literal(s)
nb_var = 4
nb_cl  = 3
nb_lit = 8

Cl[0] = (0)
Cl[1] = (3)
Cl[2] = (6)
Cl[3] = (8)

Lit[0] = 3, càd 1
Lit[1] = 4, càd -2
Lit[2] = 7, càd 3
Lit[3] = 2, càd -1
Lit[4] = 6, càd -3
Lit[5] = 9, càd 4
Lit[6] = 5, càd 2
Lit[7] = 8, càd -4

$ ./sat -T CNF CNF-files/test-001.cnf
The formula contains 4 variable(s), 3 clause(s) for a total of 8 literal(s)
1 -2 3
-1 -3 4
2 -4

L'algorithme naïf

Les solutions partielles

La plupart des algorithmes essaient d'agrandir une solution partielle jusqu'à trouver une vraie solution, ou une contradiction (auquel cas, ils reviennent en arrière). Une telle solution pourrait par exemple être "x₃=FALSE, x₁=TRUE".

Les solutions partielles sont représentées par 2 tableaux

1. Var, qui contient les (numéros des) variables de la solution actuelle, par exemple {3, 1}.

   La taille de Var, appelée n, évolue au cours de l'exécution : elle augmente lorsqu'on ajoute une variable à la solution, et elle diminue lors du backtracking quand on est arrivé à une solution incorrecte.

   La valeur de n peut devenir négative (-1) lorsque le backtracking échoue, et supérieure au nombre total de variables lorsque que l'algorithme a trouvé une solution.

2. State, de taille 1+nb_var, qui donne, pour chaque variable x₁, ..., x₄ l'état actuel de la variable : RIEN (pour les variables qui ne sont pas dans la solution partielle), VRAI ou FAUX, par exemple {RIEN, TRUE, RIEN, FALSE, RIEN, ...}

   Comme il faut se souvenir des valeurs déjà testées, il y a en fait 5 états distincts. Dans le code fourni, ces états sont appelés UNSET, FALSE, TRUE, FALSE_WAS_TRUE et TRUE_WAS_FALSE.

   Ces constantes sont des synonymes pour -1, 0, 1, 2 et 3, et on obtient (sauf pour UNSET) la valeur booléenne correspondante en regardant le bit de poids faible de l'état : State[x] & 1.

Ces données sont elles aussi stockées dans une structure :

typedef struct {
    int n;      // number of variable in the current assignement
    int* Var;   // array of variables in the current assignement: the array is of size nb_var, but
                // only the first n entries are relevant. The other ones should be UNSET (-1).
    int* State; // array of values ("states") of the variable. Variables not in the Var array should
                // have value UNSET (-1).
} sol_t;

... .... .. . .. .. . ......... ..... .
    ... . . ..
    ... .... . . .......... . . ........ . ... .... .
        ... ... . ..........
        ... . . ..............
        ... . . ..........
        .. ............ .. ..... .. ............ . .. .. .. .
            . . ..
            ......
        .
    .
    .. .. .. .. .
        ...... ..
    .
.
...... ..

$ ./sat -N CNF-files/test-001.cnf
SATISFIABLE
1 2 3 4
*** IS THAT REALLY A SOLUTION?

Le code

L'algorithme itératif naïf sur ces structure de données ressemble à

int solve_naive(formula_t* F, sol_t* S)
{
    // NOTE : S->n est initialisé à 0

    while (0 <= S->n && S->n < F->nb_var) {
        // on regarde la n-ème variable de la solution actuelle :
        if (S->Var[S->n] == UNSET) {
            // il faut choisir une variable à ajouter à la solution actuelle
            // on peut prendre les variables dans l'ordre : 1, 2, 3, .
            // (Attention au décalage de 1 : les variables commencent à 1.)
            S->Var[S->n] = S->n + 1;
            // il faut aussi choisir une valeur pour cette variable
            // on peut prendre VRAI.
            S->State[S->Var[S->n]] = TRUE;
        } else if (S->State[S->Var[S->n]] == TRUE || S->State[S->Var[S->n]] == FALSE) {
            // si la variable avait déjà une valeur, il faut en choisir une autre
            // on change la valeur de TRUE (1) à FALSE_WAS_TRUE (2) et de FALSE (0) à TRUE_WAS_FALSE
            // (3)
            S->State[S->Var[S->n]] = 3 - S->State[S->Var[S->n]];
        }

        if (is_non_false(F, S)) {
            // si les valeurs des variables ne rendent pas la formule fausse, on continue
            S->n++;
        } else {
            // sinon, il faut revenir en arrière !
            // NOTE : la fonction backtrack_naive diminue la valeur de S->n
            backtrack_naive(S);
        }
    }
    if (S->n < 0) {
        // non satisfiable
        return 0;
    } else {
        // satisfiable
        return 1;
    }
}

La fonction backtrack_naive est assez simple : elle enlève des variables d'une solution partielle pour obtenir une dernière variable dont on peut changer la valeur (càd une variable où on a testé qu'une seule valeur booléenne). Cette fonction modifie la structure S ! Il est possible que la solution renvoyée soit vide (càd avec S->n == -1). Ceci arrive lorsqu'on a testé toutes les solutions possible et que la formule n'est pas satisfiable.

int backtrack_naive(sol_t* S)
{
  // tant que la dernière variable de la solution à été testée sur les 2 valeurs
  while (S->n >= 0 && (S->State[S->Var[S->n]] == TRUE_WAS_FALSE ||
                       S->State[S->Var[S->n]] == FALSE_WAS_TRUE)) {
    S->State[S->Var[S->n]] = UNSET; // on rénitialise cette variable
    S->Var[S->n] = UNSET;           // on la supprime de la solution courante
    S->n--;
  }
  return S->n;
}

La fonction is_non_false n'est pas très difficile mais nécessite de parcourir le tableau Lit. Elle regarde si une clause est fausse, càd ne contient que des littéraux dont la valeur est FAUX. Elle ressemble donc à

int is_non_false(formula_t* F, sol_t* S)
{
    // pour toutes les clauses
    for (int cl = 0; cl < F->nb_cl; cl++) {
        // on calcule la valeur de vérité
        int clause_value = 0;
        // pour tous les littéraux de la clause
        for (int k = F->Cl[cl]; k < F->Cl[cl + 1]; k++) {
            int lit = F->Lit[k];     // littéral courant
            int x = VARIABLE(lit);   // variable correspondante
            int s = SIGN(lit);       // signe correspondant
            int v = S->State[x] & 1; // valeur de la variable dans la solution
            // si ce littéral n'est pas faux, la clause n'est pas fausse !
            if (S->State[x] == UNSET || s == v) {
                clause_value = 1;
                break;
            }
        }
        if (clause_value == 0) {
            return 0;
        }
    }
    return 1;
}

Ce code se trouve dans le fichier naive.c. Vous pouvez l'utiliser en donnant l'option -N ou --naive sur la ligne de commandes :

$ ./sat -N CNF-files/test-001.cnf
...

Pour obtenir des affichages sur le fonctionnement de l'algorithme, utilisez l'option -v ou --verbose (éventuellement plusieurs fois) :

$ ./sat -Nv CNF-files/test-001.cnf
...
$ ./sat -Nvv CNF-files/test-001.cnf
...
$ ./sat -Nvvv CNF-files/test-001.cnf
...
$ ./sat -Nvvvv CNF-files/test-001.cnf
...

1. Amélioration de la structure de données : "watch lists"

Profilage

Presque toute la complexité de la version naïve vient de la fonction is_non_false, qui parcourt à chaque fois l'intégralité du tableau Lit. La version Python du TP1 ne parcourait que des versions simplifiées de la formule, ce qui est un avantage non négligeable. (Par contre, le mécanisme de récursion nécessite de conserver en mémoire toutes les versions de la formule.)

La démarche de regarder d'où vient la complexité d'un programme de manière expérimentale s'appelle le profilage, ou profiling. Il existe des outils pour faire ceci. Deux de ces outils sont

• compilation en mode "debug", et utilisation de gprof

• compilation "normal", et utilisation de l'outils callgrind de valgrind.

Vous pouvez choisir l'un ou l'autre de ces outils pour faire la question suivante.

Utilisation de gprof

Utilisation de callgrind

1.1. "Watch lists"

Pour accélérer la fonction is_non_false, il va falloir utiliser des structures de données supplémentaires.

Une formule en FNC est fausse lorsqu'une de ses clauses ne contient que des littéraux faux. Tant que toutes les clauses contiennent au moins un littéral non faux (càd vrai ou non-instancié), on peut essayer d'étendre la solution courante.

Les "watch lists" (listes de surveillance en français) vont donner, pour chaque littéral, une liste de clauses à surveiller. Par exemple, si la "watch list" du littéral ¬x₃ contient (2), (7) et (9), cela signifie que lorsque ¬x₃ devient faux, il suffit de vérifier que les clauses (2), (7) et (9) ne sont pas devenue fausses. Au lieu de parcourir toute la formule, on ne regarde donc que 3 clauses.

Initialement, chaque clause est surveillée par son premier littéral. Par exemple, pour la formule (x₁ ∨ ¬x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃ ∨ x₄) ∧ (x₂ ∨ ¬x₄) ∧ (x₂ ∨ ¬x₁), les "watch lists" sont :

• littéral x₁ : "clause (0)" (un seul élément),

• littéral ¬x₁ : "clause (1)" (un seul élément),

• littéral x₂ : "clause (2), clause (3)" (deux éléments),

• littéraux ¬x₂, x₃, ¬x₃, x₄ et ¬x₄ : listes vides.

Si l'algorithme décide de passer la variable x₂ à FAUX, la fonction is_non_false n'aura besoin de regarder que les clauses (2) et (3). Pour ces clauses :

• il faut chercher un autre littéral dont la valeur n'est pas FAUX,

• mettre les "watch lists" à jours.

Pour cette raison, la fonction is_not_false s'appellera désormais update_watch_lists.

Par exemple, lorsque x₂ devient FAUX, la clause (2) (x₂ ∨ ¬x₄) ne peut plus apparaitre dans la "watch list" du littéral x₂. La fonction update_watch_lists devra donc :

• échanger x₂ et ¬x₄ dans la clause,

• insérer la clause (2) dans la watch list du littéral ¬x₄.

Lorsque ceci aura été fait pour les clauses 2 et 3, il faudra également vider la "watch list" du littéral x₂. Après ceci, l'invariant

sera à nouveau vérifié.

Exemples très simples

Vous devriez maintenant pouvoir tester :

$ ./sat -Wvvvv CNF-files/test-002.cnf

Benchmarks

$ ./sat -N CNF-files/queens-15-SAT.cnf
...
$ ./sat -W CNF-files/queens-15-SAT.cnf
...

$ time ./sat -N CNF-files/queens-15-SAT.cnf
...
$ time ./sat -W CNF-files/queens-15-SAT.cnf
...

$ time ./sat -W CNF-files/queens-15-SAT.cnf
...
$ time python3 ./naivesat.py -D CNF-files/queens-15-SAT.cnf
...

1.2. Liste des variables actives

L'objectif final est d'obtenir une version de l'algorithme qui détecte les clauses unitaires (celles avec un unique littéral). Pour éviter de parcourir toutes les clauses à la recherche d'une clause unitaire, nous allons utiliser une autre liste : celle des variables qui apparaissent au début d'une clause. En effet, s'il y a une clause unitaire, la variable correspondante apparait nécessairement en tête d'une clause.

Si la formule ressemble à

x₁₇ ne peut pas apparaitre dans une clause unitaire car elle a des "watch lists" vides. Seules les variables x₁ et x₂ peuvent apparaitre dans une clause unitaire.

Dans ce cas là, on pourra donc instancier x₂ à FAUX (rendant ¬x₂ VRAI). La formule deviendra alors

et x₁₇ pourra maintenant être considérée car elle a une "watch list" non vide.

La liste des variables actives (A) est initialisée par le code fourni, à condition que l'on lance le programme avec l'option -A (ou -D).

Il faut par contre gérer les mises à jours de cette liste :

1. Lors du choix d'une valeur pour une variable (fonction solve), il faut supprimer la variable de la liste des variables actives.

   • Pour cela, comme la variable choisie est la première variable active, il suffit de supprimer la première variable active (fonction pop_active).

   • Attention, il ne faut pas faire ceci lorsque la variable en question est déjà instanciée. En effet, dans ce cas, la variable a déjà été retirée des variables actives à une étape précédente. (Cette situation arrive en cas de backtracking.)

2. Lors de la mise à jours des "watch lists" (fonction update_watch_lists), la nouvelle variable qui vient en tête d'une clause peut devenir active (fonction push_active). Il faut :

   • que cette variable soit à l'état UNSET (une variable instanciée ne peut pas être active),

   • que cette variable ait des "watch list" vides (avec une "watch list" non vide, elle était déjà active).

3. Lors du backtracking (fonction backtrack), lorsqu'une variable est enlevée de la solution courante, son état devient UNSET. Si elle a une "watch list" non vide, elle doit redevenir active (fonction push_active).

2. Algorithme DPLL, avec "watch lists" et variables actives

Tout est maintenant en place pour ajouter la simplification des clauses unitaires :

• pour choisir une variable, on parcourt la liste des variables actives, et pour chacune d'entre elles, on cherche une clause unitaire dans ses "watch lists"

• si on trouve une telle clause, on force la valeur de sa première variable (état FORCED_FALSE ou FORCED_TRUE),

• si on n'en trouve pas, on prend la première variable active

• et c'est tout !

2.1. Recherche des clauses unitaires

2.2. Quelques tests

Le répertoire CNF-files contient de nombreux fichiers, et en particulier des fichiers "de plus en plus gros" :

• les fichiers CNF-files/queens-N-SAT.cnf (pour plusieurs valeurs de N) contiennent l'encodage en formule CNF du problème des N reines,

• les fichiers CNF-files/multiplication-B-N.cnf contiennent l'encodage de la multiplication de 2 nombres de B bits pour obtenir un résultat de N,

• les fichiers CNF-files/sudoku-easy-N.cnf et CNF-files/sudoku-hard-N.cnf contiennent l'encodage de grilles de sudoku classées "facile" ou "difficile".

$ minisat FICHIER.cnf

Remarques sur la page (ou le sujet) : contact.
mentions légales

,

Dernière révision: le 19-11-2020 à 11:16.