Samedi 14 octobre 2023

• Programme pour le problème Couverture par sommets (page actuelle)
• Programme pour le problème Arbre à k feuilles

Télécharger, compiler et exécuter

vertex-cover.c | sat-solver.c

Les fichiers utilisent la mini bibliothèque HandyMacros faite par bibi. Vous pouvez télécharger, compiler et exécuter en trois commandes :

wget https://sylvain-chiron.emi.u-bordeaux.fr/coca/vertex-cover.c https://sylvain-chiron.emi.u-bordeaux.fr/coca/sat-solver.c \
   https://gitlab.com/Frigory33/handymacros/-/raw/master/src/handymacros.h https://gitlab.com/Frigory33/handymacros/-/raw/master/src/handymacros.c
cc -o vertex-cover vertex-cover.c handymacros.c -I . -Wall -O2
./vertex-cover $mode help
   

Si vous n’avez pas Wget, téléchargez les fichiers à la main au lieu d’exécuter la première commande. La bibliothèque peut éventuellement être installée avec make install sous les environnements Unix, lorsque vous avez téléchargé le dépôt.

Le programme vertex-cover a quatre modes :

• mode= : le programme résout le problème sur une instance, en donnant un certificat le cas échéant ;
• mode=verify : le programme vérifie une proposition de certificat pour une instance ;
• mode=reduce : le programme génère une réduction vers CNF-SAT pour une instance ;
• mode=valuation : le programme génère une valuation correspondant à une instance et une proposition de certificat, qui colle avec la réduction vers SAT.

Supprimez l’argument help pour n’avoir que des invites minimales autour de la saisie de votre entrée (ce qui permet de facilement la copier-coller pour la réutiliser, par exemple).

Lorsque vous avez une réduction vers SAT, vous pouvez compiler et exécuter votre sat-solver de cette façon :

cc -o sat-solver sat-solver.c handymacros.c -x c - -I . -Wall -O2 -D VERTEX_COVER
./sat-solver
   

Vous pouvez remplacer -x c - par un nom de fichier .c pour utiliser celui-ci plutôt que l’entrée standard. Sinon, il vous est possible de coller directement votre code dans l’entrée standard. Voir plus bas le format que doit avoir le fichier.

Présentation

Le problème Couverture par sommets est abordé à l’exercice 2.3 des TD du cours d’Anca Muscholl. Les trois premiers modes sont les algorithmes demandés ou suggérés par les trois premières questions.

Je ne l’ai testé que sur des graphes nuls et sur ce tout petit graphe G :

L’entrée correspondante est :

3 2
0 1
1 2
   

L’entrée suit un format semblable à ce qu’on retrouve classiquement dans les exercices d’algorithmique en ligne ou en concours, par exemple sur France-IOI, Prologin, Project Euler, CodeForces et Primers. Le programme n’est pas fait pour gérer les entrées invalides : elles peuvent le faire planter.

Bien entendu, il est possible d’utiliser des redirections vers des fichiers au lieu de toujours faire la saisie dans le terminal.

Exemples d’exécution

La sortie est en noir et l’entrée en rouge.

$ ./vertex-cover help
Instance :
   Graphe :
      Nb sommets et arêtes : 3 2
      Arête : 0 1
      Arête : 1 2
   Nb sommets requis : 1
Réponse : Oui
Certificat :
   Sommets : 1
      

$ ./vertex-cover
Instance :
0 0
1
Réponse : Non
      

$ ./vertex-cover verify help
Instance :
   Graphe :
      Nb sommets et arêtes : 3 2
      Arête : 0 1
      Arête : 1 2
   Nb sommets requis : 1
Valeurs :
   Nb sommets : 1
   Sommets : 0
Ça ne passe pas
      

$ ./vertex-cover verify
Instance :
0 0
0
Valeurs :
0
Ça passe
      

$ ./vertex-cover reduce
Instance :
0 0
0
Réduction :
(
   true
) &&
(
   true
) &&
(
   true
) &&
(
   true
)
      

$ ./vertex-cover reduce
Instance :
0 0
1
Réduction :
(
   true
) &&
(
   true &&
   (false)
) &&
(
   true &&
   (
      true
   )
) &&
(
   true
)
      

$ ./vertex-cover reduce
Instance :
3 2
0 1
1 2
0
Réduction :
(
   true &&
   (
      false
   ) &&
   (
      false
   )
) &&
(
   true
) &&
(
   true
) &&
(
   true &&
   (
      true
   ) &&
   (
      true
   ) &&
   (
      true
   )
)
      

$ ./vertex-cover reduce
Instance :
3 2
0 1
1 2
1
Réduction :
(
   true &&
   (
      false ||
      x[0][0] || x[1][0]
   ) &&
   (
      false ||
      x[1][0] || x[2][0]
   )
) &&
(
   true &&
   (false || x[0][0] || x[1][0] || x[2][0])
) &&
(
   true &&
   (
      true &&
      (!x[0][0] || !x[1][0]) &&
      (!x[0][0] || !x[2][0]) &&
      (!x[1][0] || !x[2][0])
   )
) &&
(
   true &&
   (
      true
   ) &&
   (
      true
   ) &&
   (
      true
   )
)
      

$ ./vertex-cover reduce
Instance :
3 2
0 1
1 2
2
Réduction :
(
   true &&
   (
      false ||
      x[0][0] || x[1][0] ||
      x[0][1] || x[1][1]
   ) &&
   (
      false ||
      x[1][0] || x[2][0] ||
      x[1][1] || x[2][1]
   )
) &&
(
   true &&
   (false || x[0][0] || x[1][0] || x[2][0]) &&
   (false || x[0][1] || x[1][1] || x[2][1])
) &&
(
   true &&
   (
      true &&
      (!x[0][0] || !x[1][0]) &&
      (!x[0][0] || !x[2][0]) &&
      (!x[1][0] || !x[2][0])
   ) &&
   (
      true &&
      (!x[0][1] || !x[1][1]) &&
      (!x[0][1] || !x[2][1]) &&
      (!x[1][1] || !x[2][1])
   )
) &&
(
   true &&
   (
      true &&
      (!x[0][0] || !x[0][1])
   ) &&
   (
      true &&
      (!x[1][0] || !x[1][1])
   ) &&
   (
      true &&
      (!x[2][0] || !x[2][1])
   )
)
      

$ ./vertex-cover valuation
Instance :
3 2
0 1
1 2
2
Valeurs :
2
1 1
Valuation :
   bool x[3][2] = {
         [1][0] = true,
         [1][1] = true,
      };
      

$ ./vertex-cover valuation
Instance :
0 0
2
Valeurs :
0
Valuation :
   bool x[1][2] = {
      };
      

Utilisation des expressions de réduction et des valuations

Les expressions générées par les fonctionnalités de réduction et de valuation peuvent être utilisées dans un programme de ce type :

#include <stdio.h>
#include <handymacros.h>

int main()
{
   // Mettez la valuation ici
   bool ok =
         // Mettez l’expression ici
      ;

   if (ok) {
      printf("Valuation satisfaisante\nSommets :");
      for_range (int, vert, 0, < array_len(x), ++) {
         for_array (bool, val, x[vert]) {
            if (val) {
               printf(" %d", vert);
            }
         }
      }
      printf("\n");
   } else {
      printf("Valuation non satisfaisante\n");
   }
}
   

Notez que toutes les valuations insatisfaisantes ne peuvent pas être générées par le programme.

Pour utiliser le solveur SAT (plutôt que coder la valuation en dur), vous devez lui fournir trois éléments : le nombre de sommets du graphe, la taille que doit avoir l’ensemble de sommets couvrants et la fonction de test. Votre fichier source doit suivre ce format :

#include <handymacros.h>

size_t const nbVert = /* nombre de sommets */, requiredSize = /* taille de l’ensemble */;

bool vertexCoverTest(bool x[nbVert][requiredSize])
{
   return /* expression */;
}
   

Le solveur SAT est le solveur basique qui teste bêtement toutes les possibilités.

Explications

L’algorithme de réduction vers SAT

L’idée est d’abord d’avoir une variable booléenne pour chaque sommet afin de représenter l’ensemble testé : la variable vaut vrai si le sommet est dans l’ensemble et faux sinon. Cela donne un tableau équivalent à selectedVertices dans le code source du programme. On a alors un x_u pour chaque u. Pour que l’ensemble soit couvrant, il faut, pour chaque arête (u, v) : x_u ∨ x_v. C’est la première contrainte, placée dans la première grande paire de parenthèses dans les résultats du programme.

Cela ne permet pas de garantir que l’ensemble est de taille p. Pour le faire, on multiplie le nombre de variables par p et on pose :

x_u = x_u,0 ∨ x_u,1 ∨ … ∨ x_u,p-1

Tous les x_u sont ainsi substitués. Chaque x_u,i indique si le sommet u est dans l’ensemble à la position i. Cela signifie qu’on se représente l’ensemble comme une liste de sommets de taille p. Il faut alors ajouter trois contraintes pour s’assurer que cette liste constitue un ensemble valide. Pour être valide, l’ensemble doit respecter ces trois conditions :

• à chaque position, il y a au moins un sommet ;
• à chaque position, il y a au plus un sommet ;
• chaque sommet apparait au plus une fois.

C’est ce que codent les trois dernières grandes paires de parenthèses. Les deux « au plus » se codent en testant, pour chaque position ou sommet, toutes les paires possibles de sommets ou positions respectivement, afin de vérifier qu’il n’y a pas de conflit au sein d’une de ces paires.

L’algorithme ne voit aucun cas comme particulier. Par conséquent, des true && ou false || sont toujours ajoutés au cas où une itération se fait sur un ensemble vide.