Programme pour le problème Arbre à k feuilles

Lundi 30 octobre 2023

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

Télécharger, compiler et exécuter

Ce programme suit le même modèle que le programme pour le problème Couverture par sommets : il offre les mêmes fonctionnalités pour le problème Arbre à k feuilles.

wget https://sylvain-chiron.emi.u-bordeaux.fr/coca/k-leafs-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 k-leafs-cover k-leafs-cover.c handymacros.c -I . -Wall -O2
./k-leafs-cover $mode help

Rappel des quatre modes : rien (résoudre), verify, reduce et valuation. Cette fois, la réduction vers SAT ne donne pas une formule CNF.

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 K_LEAFS_COVER
./sat-solver

Voir plus bas le format que doit avoir le fichier d’entrée.

Voir le code source

Présentation

Le problème Arbre à k feuilles a été le sujet du devoir surveillé du 23 octobre. On nous y a demandé de décrire le fonctionnement d’un vérificateur pour ce problème, et de compléter un algorithme de réduction de ce problème vers SAT.

Le problème correspond à la question suivante : « Pour un graphe donné et un entier k, existe-t-il un arbre couvrant ce graphe qui a exactement k feuilles ? » Par exemple, sur le graphe G₁ ci-dessous, les arêtes bleues correspondent à un arbre couvrant à 3 feuilles.

Les informations déjà présentes sur la page du programme pour le problème Couverture par sommets ne sont pas répétées ici.

Les exemples de la section suivante sont faits avec les deux graphes ci-dessous :

G₁		5 7 0 1 0 2 0 3 0 4 2 3 2 4 3 4
G₂		6 6 1 2 2 3 3 4 0 3 3 5 5 0

Exemples d’exécution

Résolution

Résolutions pour le graphe G₁ :

$ ./k-leafs-cover help
Instance :
   Graphe :
      Nb sommets et arêtes : 5 7
      Arête : 0 1
      Arête : 0 2
      Arête : 0 3
      Arête : 0 4
      Arête : 2 3
      Arête : 2 4
      Arête : 3 4
   Nb feuilles voulues : 4
Réponse : Oui
Certificat :
   Arêtes : 0 1 2 3

$ ./k-leafs-cover
Instance :
5 7
0 1
0 2
0 3
0 4
2 3
2 4
3 4
3
Réponse : Oui
Certificat :
   Arêtes : 0 1 2 5

$ ./k-leafs-cover
Instance :
5 7
0 1
0 2
0 3
0 4
2 3
2 4
3 4
2
Réponse : Oui
Certificat :
   Arêtes : 0 1 4 6

Résolutions pour le graphe G₂ :

$ ./k-leafs-cover
Instance :
6 6
1 2
2 3
3 4
0 3
3 5
5 0
4
Réponse : Oui
Certificat :
   Arêtes : 0 1 2 3 4

$ ./k-leafs-cover
Instance :
6 6
1 2
2 3
3 4
0 3
3 5
5 0
3
Réponse : Oui
Certificat :
   Arêtes : 0 1 2 3 5

$ ./k-leafs-cover
Instance :
6 6
1 2
2 3
3 4
0 3
3 5
5 0
2
Réponse : Non

Vérification

Vérifications de la sélection (les arêtes bleues) sur le graphe G₁ :

$ ./k-leafs-cover verify help
Instance :
   Graphe :
      Nb sommets et arêtes : 5 7
      Arête : 0 1
      Arête : 0 2
      Arête : 0 3
      Arête : 0 4
      Arête : 2 3
      Arête : 2 4
      Arête : 3 4
   Nb feuilles voulues : 3
Valeurs :
   Nb arêtes : 4
   Arêtes (par n°) : 4 5 0 1
Ça passe

Instance :
5 7
0 1
0 2
0 3
0 4
2 3
2 4
3 4
4
Valeurs :
4
4 5 0 1
Ça ne passe pas

Réduction

Réduction pour le petit graphe G du problème Couverture par sommets :

$ ./k-leafs-cover reduce
Instance :
3 2
0 1
1 2
2
Réduction :
( // φ1
   (
      true &&
      (false || y[0][0] || y[1][0] || y[2][0]) &&
      (false || y[0][1] || y[1][1] || y[2][1])
   ) &&
   (
      true &&
      (
         true &&
         (!y[0][0] || !y[1][0]) &&
         (!y[0][0] || !y[2][0]) &&
         (!y[1][0] || !y[2][0])
      ) &&
      (
         true &&
         (!y[0][1] || !y[1][1]) &&
         (!y[0][1] || !y[2][1]) &&
         (!y[1][1] || !y[2][1])
      )
   ) &&
   (
      true &&
      (
         true &&
         (!y[0][0] || !y[0][1])
      ) &&
      (
         true &&
         (!y[1][0] || !y[1][1])
      ) &&
      (
         true &&
         (!y[2][0] || !y[2][1])
      )
   )
) &&
( // φ2
   true &&
   (
      z[1][0][0] == (false || y[0][0] || y[0][1]) &&
      (
         true &&
         z[1][0][1] == (z[1][0][0] || (z[0][0][0] && z[1][0][0])) &&
         z[1][0][2] == (z[1][0][1] || (z[0][1][1] && z[1][1][1])) &&
         z[1][0][3] == (z[1][0][2] || (z[0][2][2] && z[1][2][2]))
      ) &&
      z[1][0][3]
   ) &&
   (
      !z[2][0][0] &&
      (
         true &&
         z[2][0][1] == (z[2][0][0] || (z[0][0][0] && z[2][0][0])) &&
         z[2][0][2] == (z[2][0][1] || (z[0][1][1] && z[2][1][1])) &&
         z[2][0][3] == (z[2][0][2] || (z[0][2][2] && z[2][2][2]))
      ) &&
      z[2][0][3]
   ) &&
   (
      z[2][1][0] == (false || y[1][0] || y[1][1]) &&
      (
         true &&
         z[2][1][1] == (z[2][1][0] || (z[1][0][0] && z[2][0][0])) &&
         z[2][1][2] == (z[2][1][1] || (z[1][1][1] && z[2][1][1])) &&
         z[2][1][3] == (z[2][1][2] || (z[1][2][2] && z[2][2][2]))
      ) &&
      z[2][1][3]
   )
) &&
( // φ3
   (
      true &&
      (
         (false || x[0][0] || x[0][1]) ==
         (
            true &&
            (!z[1][0][0] || !z[2][0][0])
         )
      ) &&
      (
         (false || x[1][0] || x[1][1]) ==
         (
            true &&
            (!z[1][0][0] || !z[2][1][0])
         )
      ) &&
      (
         (false || x[2][0] || x[2][1]) ==
         (
            true &&
            (!z[2][0][0] || !z[2][1][0])
         )
      )
   ) &&
   (
      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])
      )
   )
)

Réduction pour le graphe G₂ :

$ ./k-leafs-cover reduce
Instance :
6 6
1 2
2 3
3 4
0 3
3 5
5 0
3
Réduction :
( // φ1
   (
      true &&
      (false || y[0][0] || y[1][0] || y[2][0] || y[3][0] || y[4][0] || y[5][0]) &&
      (false || y[0][1] || y[1][1] || y[2][1] || y[3][1] || y[4][1] || y[5][1]) &&
      (false || y[0][2] || y[1][2] || y[2][2] || y[3][2] || y[4][2] || y[5][2]) &&
      (false || y[0][3] || y[1][3] || y[2][3] || y[3][3] || y[4][3] || y[5][3]) &&
      (false || y[0][4] || y[1][4] || y[2][4] || y[3][4] || y[4][4] || y[5][4])
   ) &&
   (
      true &&
      (
         true &&
         (!y[0][0] || !y[1][0]) &&
         (!y[0][0] || !y[2][0]) &&
         (!y[0][0] || !y[3][0]) &&
         (!y[0][0] || !y[4][0]) &&
         (!y[0][0] || !y[5][0]) &&
         (!y[1][0] || !y[2][0]) &&
         (!y[1][0] || !y[3][0]) &&
         (!y[1][0] || !y[4][0]) &&
         (!y[1][0] || !y[5][0]) &&
         (!y[2][0] || !y[3][0]) &&
         (!y[2][0] || !y[4][0]) &&
         (!y[2][0] || !y[5][0]) &&
         (!y[3][0] || !y[4][0]) &&
         (!y[3][0] || !y[5][0]) &&
         (!y[4][0] || !y[5][0])
      ) &&
      (
         true &&
         (!y[0][1] || !y[1][1]) &&
         (!y[0][1] || !y[2][1]) &&
         (!y[0][1] || !y[3][1]) &&
         (!y[0][1] || !y[4][1]) &&
         (!y[0][1] || !y[5][1]) &&
         (!y[1][1] || !y[2][1]) &&
         (!y[1][1] || !y[3][1]) &&
         (!y[1][1] || !y[4][1]) &&
         (!y[1][1] || !y[5][1]) &&
         (!y[2][1] || !y[3][1]) &&
         (!y[2][1] || !y[4][1]) &&
         (!y[2][1] || !y[5][1]) &&
         (!y[3][1] || !y[4][1]) &&
         (!y[3][1] || !y[5][1]) &&
         (!y[4][1] || !y[5][1])
      ) &&
      (
         true &&
         (!y[0][2] || !y[1][2]) &&
         (!y[0][2] || !y[2][2]) &&
         (!y[0][2] || !y[3][2]) &&
         (!y[0][2] || !y[4][2]) &&
         (!y[0][2] || !y[5][2]) &&
         (!y[1][2] || !y[2][2]) &&
         (!y[1][2] || !y[3][2]) &&
         (!y[1][2] || !y[4][2]) &&
         (!y[1][2] || !y[5][2]) &&
         (!y[2][2] || !y[3][2]) &&
         (!y[2][2] || !y[4][2]) &&
         (!y[2][2] || !y[5][2]) &&
         (!y[3][2] || !y[4][2]) &&
         (!y[3][2] || !y[5][2]) &&
         (!y[4][2] || !y[5][2])
      ) &&
      (
         true &&
         (!y[0][3] || !y[1][3]) &&
         (!y[0][3] || !y[2][3]) &&
         (!y[0][3] || !y[3][3]) &&
         (!y[0][3] || !y[4][3]) &&
         (!y[0][3] || !y[5][3]) &&
         (!y[1][3] || !y[2][3]) &&
         (!y[1][3] || !y[3][3]) &&
         (!y[1][3] || !y[4][3]) &&
         (!y[1][3] || !y[5][3]) &&
         (!y[2][3] || !y[3][3]) &&
         (!y[2][3] || !y[4][3]) &&
         (!y[2][3] || !y[5][3]) &&
         (!y[3][3] || !y[4][3]) &&
         (!y[3][3] || !y[5][3]) &&
         (!y[4][3] || !y[5][3])
      ) &&
      (
         true &&
         (!y[0][4] || !y[1][4]) &&
         (!y[0][4] || !y[2][4]) &&
         (!y[0][4] || !y[3][4]) &&
         (!y[0][4] || !y[4][4]) &&
         (!y[0][4] || !y[5][4]) &&
         (!y[1][4] || !y[2][4]) &&
         (!y[1][4] || !y[3][4]) &&
         (!y[1][4] || !y[4][4]) &&
         (!y[1][4] || !y[5][4]) &&
         (!y[2][4] || !y[3][4]) &&
         (!y[2][4] || !y[4][4]) &&
         (!y[2][4] || !y[5][4]) &&
         (!y[3][4] || !y[4][4]) &&
         (!y[3][4] || !y[5][4]) &&
         (!y[4][4] || !y[5][4])
      )
   ) &&
   (
      true &&
      (
         true &&
         (!y[0][0] || !y[0][1]) &&
         (!y[0][0] || !y[0][2]) &&
         (!y[0][0] || !y[0][3]) &&
         (!y[0][0] || !y[0][4]) &&
         (!y[0][1] || !y[0][2]) &&
         (!y[0][1] || !y[0][3]) &&
         (!y[0][1] || !y[0][4]) &&
         (!y[0][2] || !y[0][3]) &&
         (!y[0][2] || !y[0][4]) &&
         (!y[0][3] || !y[0][4])
      ) &&
      (
         true &&
         (!y[1][0] || !y[1][1]) &&
         (!y[1][0] || !y[1][2]) &&
         (!y[1][0] || !y[1][3]) &&
         (!y[1][0] || !y[1][4]) &&
         (!y[1][1] || !y[1][2]) &&
         (!y[1][1] || !y[1][3]) &&
         (!y[1][1] || !y[1][4]) &&
         (!y[1][2] || !y[1][3]) &&
         (!y[1][2] || !y[1][4]) &&
         (!y[1][3] || !y[1][4])
      ) &&
      (
         true &&
         (!y[2][0] || !y[2][1]) &&
         (!y[2][0] || !y[2][2]) &&
         (!y[2][0] || !y[2][3]) &&
         (!y[2][0] || !y[2][4]) &&
         (!y[2][1] || !y[2][2]) &&
         (!y[2][1] || !y[2][3]) &&
         (!y[2][1] || !y[2][4]) &&
         (!y[2][2] || !y[2][3]) &&
         (!y[2][2] || !y[2][4]) &&
         (!y[2][3] || !y[2][4])
      ) &&
      (
         true &&
         (!y[3][0] || !y[3][1]) &&
         (!y[3][0] || !y[3][2]) &&
         (!y[3][0] || !y[3][3]) &&
         (!y[3][0] || !y[3][4]) &&
         (!y[3][1] || !y[3][2]) &&
         (!y[3][1] || !y[3][3]) &&
         (!y[3][1] || !y[3][4]) &&
         (!y[3][2] || !y[3][3]) &&
         (!y[3][2] || !y[3][4]) &&
         (!y[3][3] || !y[3][4])
      ) &&
      (
         true &&
         (!y[4][0] || !y[4][1]) &&
         (!y[4][0] || !y[4][2]) &&
         (!y[4][0] || !y[4][3]) &&
         (!y[4][0] || !y[4][4]) &&
         (!y[4][1] || !y[4][2]) &&
         (!y[4][1] || !y[4][3]) &&
         (!y[4][1] || !y[4][4]) &&
         (!y[4][2] || !y[4][3]) &&
         (!y[4][2] || !y[4][4]) &&
         (!y[4][3] || !y[4][4])
      ) &&
      (
         true &&
         (!y[5][0] || !y[5][1]) &&
         (!y[5][0] || !y[5][2]) &&
         (!y[5][0] || !y[5][3]) &&
         (!y[5][0] || !y[5][4]) &&
         (!y[5][1] || !y[5][2]) &&
         (!y[5][1] || !y[5][3]) &&
         (!y[5][1] || !y[5][4]) &&
         (!y[5][2] || !y[5][3]) &&
         (!y[5][2] || !y[5][4]) &&
         (!y[5][3] || !y[5][4])
      )
   )
) &&
( // φ2
   true &&
   (
      !z[1][0][0] &&
      (
         true &&
         z[1][0][1] == (z[1][0][0] || (z[0][0][0] && z[1][0][0])) &&
         z[1][0][2] == (z[1][0][1] || (z[0][1][1] && z[1][1][1])) &&
         z[1][0][3] == (z[1][0][2] || (z[0][2][2] && z[1][2][2])) &&
         z[1][0][4] == (z[1][0][3] || (z[0][3][3] && z[1][3][3])) &&
         z[1][0][5] == (z[1][0][4] || (z[0][4][4] && z[1][4][4])) &&
         z[1][0][6] == (z[1][0][5] || (z[0][5][5] && z[1][5][5]))
      ) &&
      z[1][0][6]
   ) &&
   (
      !z[2][0][0] &&
      (
         true &&
         z[2][0][1] == (z[2][0][0] || (z[0][0][0] && z[2][0][0])) &&
         z[2][0][2] == (z[2][0][1] || (z[0][1][1] && z[2][1][1])) &&
         z[2][0][3] == (z[2][0][2] || (z[0][2][2] && z[2][2][2])) &&
         z[2][0][4] == (z[2][0][3] || (z[0][3][3] && z[2][3][3])) &&
         z[2][0][5] == (z[2][0][4] || (z[0][4][4] && z[2][4][4])) &&
         z[2][0][6] == (z[2][0][5] || (z[0][5][5] && z[2][5][5]))
      ) &&
      z[2][0][6]
   ) &&
   (
      z[3][0][0] == (false || y[3][0] || y[3][1] || y[3][2] || y[3][3] || y[3][4]) &&
      (
         true &&
         z[3][0][1] == (z[3][0][0] || (z[0][0][0] && z[3][0][0])) &&
         z[3][0][2] == (z[3][0][1] || (z[0][1][1] && z[3][1][1])) &&
         z[3][0][3] == (z[3][0][2] || (z[0][2][2] && z[3][2][2])) &&
         z[3][0][4] == (z[3][0][3] || (z[0][3][3] && z[3][3][3])) &&
         z[3][0][5] == (z[3][0][4] || (z[0][4][4] && z[3][4][4])) &&
         z[3][0][6] == (z[3][0][5] || (z[0][5][5] && z[3][5][5]))
      ) &&
      z[3][0][6]
   ) &&
   (
      !z[4][0][0] &&
      (
         true &&
         z[4][0][1] == (z[4][0][0] || (z[0][0][0] && z[4][0][0])) &&
         z[4][0][2] == (z[4][0][1] || (z[0][1][1] && z[4][1][1])) &&
         z[4][0][3] == (z[4][0][2] || (z[0][2][2] && z[4][2][2])) &&
         z[4][0][4] == (z[4][0][3] || (z[0][3][3] && z[4][3][3])) &&
         z[4][0][5] == (z[4][0][4] || (z[0][4][4] && z[4][4][4])) &&
         z[4][0][6] == (z[4][0][5] || (z[0][5][5] && z[4][5][5]))
      ) &&
      z[4][0][6]
   ) &&
   (
      z[5][0][0] == (false || y[5][0] || y[5][1] || y[5][2] || y[5][3] || y[5][4]) &&
      (
         true &&
         z[5][0][1] == (z[5][0][0] || (z[0][0][0] && z[5][0][0])) &&
         z[5][0][2] == (z[5][0][1] || (z[0][1][1] && z[5][1][1])) &&
         z[5][0][3] == (z[5][0][2] || (z[0][2][2] && z[5][2][2])) &&
         z[5][0][4] == (z[5][0][3] || (z[0][3][3] && z[5][3][3])) &&
         z[5][0][5] == (z[5][0][4] || (z[0][4][4] && z[5][4][4])) &&
         z[5][0][6] == (z[5][0][5] || (z[0][5][5] && z[5][5][5]))
      ) &&
      z[5][0][6]
   ) &&
   (
      z[2][1][0] == (false || y[0][0] || y[0][1] || y[0][2] || y[0][3] || y[0][4]) &&
      (
         true &&
         z[2][1][1] == (z[2][1][0] || (z[1][0][0] && z[2][0][0])) &&
         z[2][1][2] == (z[2][1][1] || (z[1][1][1] && z[2][1][1])) &&
         z[2][1][3] == (z[2][1][2] || (z[1][2][2] && z[2][2][2])) &&
         z[2][1][4] == (z[2][1][3] || (z[1][3][3] && z[2][3][3])) &&
         z[2][1][5] == (z[2][1][4] || (z[1][4][4] && z[2][4][4])) &&
         z[2][1][6] == (z[2][1][5] || (z[1][5][5] && z[2][5][5]))
      ) &&
      z[2][1][6]
   ) &&
   (
      !z[3][1][0] &&
      (
         true &&
         z[3][1][1] == (z[3][1][0] || (z[1][0][0] && z[3][0][0])) &&
         z[3][1][2] == (z[3][1][1] || (z[1][1][1] && z[3][1][1])) &&
         z[3][1][3] == (z[3][1][2] || (z[1][2][2] && z[3][2][2])) &&
         z[3][1][4] == (z[3][1][3] || (z[1][3][3] && z[3][3][3])) &&
         z[3][1][5] == (z[3][1][4] || (z[1][4][4] && z[3][4][4])) &&
         z[3][1][6] == (z[3][1][5] || (z[1][5][5] && z[3][5][5]))
      ) &&
      z[3][1][6]
   ) &&
   (
      !z[4][1][0] &&
      (
         true &&
         z[4][1][1] == (z[4][1][0] || (z[1][0][0] && z[4][0][0])) &&
         z[4][1][2] == (z[4][1][1] || (z[1][1][1] && z[4][1][1])) &&
         z[4][1][3] == (z[4][1][2] || (z[1][2][2] && z[4][2][2])) &&
         z[4][1][4] == (z[4][1][3] || (z[1][3][3] && z[4][3][3])) &&
         z[4][1][5] == (z[4][1][4] || (z[1][4][4] && z[4][4][4])) &&
         z[4][1][6] == (z[4][1][5] || (z[1][5][5] && z[4][5][5]))
      ) &&
      z[4][1][6]
   ) &&
   (
      !z[5][1][0] &&
      (
         true &&
         z[5][1][1] == (z[5][1][0] || (z[1][0][0] && z[5][0][0])) &&
         z[5][1][2] == (z[5][1][1] || (z[1][1][1] && z[5][1][1])) &&
         z[5][1][3] == (z[5][1][2] || (z[1][2][2] && z[5][2][2])) &&
         z[5][1][4] == (z[5][1][3] || (z[1][3][3] && z[5][3][3])) &&
         z[5][1][5] == (z[5][1][4] || (z[1][4][4] && z[5][4][4])) &&
         z[5][1][6] == (z[5][1][5] || (z[1][5][5] && z[5][5][5]))
      ) &&
      z[5][1][6]
   ) &&
   (
      z[3][2][0] == (false || y[1][0] || y[1][1] || y[1][2] || y[1][3] || y[1][4]) &&
      (
         true &&
         z[3][2][1] == (z[3][2][0] || (z[2][0][0] && z[3][0][0])) &&
         z[3][2][2] == (z[3][2][1] || (z[2][1][1] && z[3][1][1])) &&
         z[3][2][3] == (z[3][2][2] || (z[2][2][2] && z[3][2][2])) &&
         z[3][2][4] == (z[3][2][3] || (z[2][3][3] && z[3][3][3])) &&
         z[3][2][5] == (z[3][2][4] || (z[2][4][4] && z[3][4][4])) &&
         z[3][2][6] == (z[3][2][5] || (z[2][5][5] && z[3][5][5]))
      ) &&
      z[3][2][6]
   ) &&
   (
      !z[4][2][0] &&
      (
         true &&
         z[4][2][1] == (z[4][2][0] || (z[2][0][0] && z[4][0][0])) &&
         z[4][2][2] == (z[4][2][1] || (z[2][1][1] && z[4][1][1])) &&
         z[4][2][3] == (z[4][2][2] || (z[2][2][2] && z[4][2][2])) &&
         z[4][2][4] == (z[4][2][3] || (z[2][3][3] && z[4][3][3])) &&
         z[4][2][5] == (z[4][2][4] || (z[2][4][4] && z[4][4][4])) &&
         z[4][2][6] == (z[4][2][5] || (z[2][5][5] && z[4][5][5]))
      ) &&
      z[4][2][6]
   ) &&
   (
      !z[5][2][0] &&
      (
         true &&
         z[5][2][1] == (z[5][2][0] || (z[2][0][0] && z[5][0][0])) &&
         z[5][2][2] == (z[5][2][1] || (z[2][1][1] && z[5][1][1])) &&
         z[5][2][3] == (z[5][2][2] || (z[2][2][2] && z[5][2][2])) &&
         z[5][2][4] == (z[5][2][3] || (z[2][3][3] && z[5][3][3])) &&
         z[5][2][5] == (z[5][2][4] || (z[2][4][4] && z[5][4][4])) &&
         z[5][2][6] == (z[5][2][5] || (z[2][5][5] && z[5][5][5]))
      ) &&
      z[5][2][6]
   ) &&
   (
      z[4][3][0] == (false || y[2][0] || y[2][1] || y[2][2] || y[2][3] || y[2][4]) &&
      (
         true &&
         z[4][3][1] == (z[4][3][0] || (z[3][0][0] && z[4][0][0])) &&
         z[4][3][2] == (z[4][3][1] || (z[3][1][1] && z[4][1][1])) &&
         z[4][3][3] == (z[4][3][2] || (z[3][2][2] && z[4][2][2])) &&
         z[4][3][4] == (z[4][3][3] || (z[3][3][3] && z[4][3][3])) &&
         z[4][3][5] == (z[4][3][4] || (z[3][4][4] && z[4][4][4])) &&
         z[4][3][6] == (z[4][3][5] || (z[3][5][5] && z[4][5][5]))
      ) &&
      z[4][3][6]
   ) &&
   (
      z[5][3][0] == (false || y[4][0] || y[4][1] || y[4][2] || y[4][3] || y[4][4]) &&
      (
         true &&
         z[5][3][1] == (z[5][3][0] || (z[3][0][0] && z[5][0][0])) &&
         z[5][3][2] == (z[5][3][1] || (z[3][1][1] && z[5][1][1])) &&
         z[5][3][3] == (z[5][3][2] || (z[3][2][2] && z[5][2][2])) &&
         z[5][3][4] == (z[5][3][3] || (z[3][3][3] && z[5][3][3])) &&
         z[5][3][5] == (z[5][3][4] || (z[3][4][4] && z[5][4][4])) &&
         z[5][3][6] == (z[5][3][5] || (z[3][5][5] && z[5][5][5]))
      ) &&
      z[5][3][6]
   ) &&
   (
      !z[5][4][0] &&
      (
         true &&
         z[5][4][1] == (z[5][4][0] || (z[4][0][0] && z[5][0][0])) &&
         z[5][4][2] == (z[5][4][1] || (z[4][1][1] && z[5][1][1])) &&
         z[5][4][3] == (z[5][4][2] || (z[4][2][2] && z[5][2][2])) &&
         z[5][4][4] == (z[5][4][3] || (z[4][3][3] && z[5][3][3])) &&
         z[5][4][5] == (z[5][4][4] || (z[4][4][4] && z[5][4][4])) &&
         z[5][4][6] == (z[5][4][5] || (z[4][5][5] && z[5][5][5]))
      ) &&
      z[5][4][6]
   )
) &&
( // φ3
   (
      true &&
      (
         (false || x[0][0] || x[0][1] || x[0][2]) ==
         (
            true &&
            (!z[1][0][0] || !z[2][0][0]) &&
            (!z[1][0][0] || !z[3][0][0]) &&
            (!z[1][0][0] || !z[4][0][0]) &&
            (!z[1][0][0] || !z[5][0][0]) &&
            (!z[2][0][0] || !z[3][0][0]) &&
            (!z[2][0][0] || !z[4][0][0]) &&
            (!z[2][0][0] || !z[5][0][0]) &&
            (!z[3][0][0] || !z[4][0][0]) &&
            (!z[3][0][0] || !z[5][0][0]) &&
            (!z[4][0][0] || !z[5][0][0])
         )
      ) &&
      (
         (false || x[1][0] || x[1][1] || x[1][2]) ==
         (
            true &&
            (!z[1][0][0] || !z[2][1][0]) &&
            (!z[1][0][0] || !z[3][1][0]) &&
            (!z[1][0][0] || !z[4][1][0]) &&
            (!z[1][0][0] || !z[5][1][0]) &&
            (!z[2][1][0] || !z[3][1][0]) &&
            (!z[2][1][0] || !z[4][1][0]) &&
            (!z[2][1][0] || !z[5][1][0]) &&
            (!z[3][1][0] || !z[4][1][0]) &&
            (!z[3][1][0] || !z[5][1][0]) &&
            (!z[4][1][0] || !z[5][1][0])
         )
      ) &&
      (
         (false || x[2][0] || x[2][1] || x[2][2]) ==
         (
            true &&
            (!z[2][0][0] || !z[2][1][0]) &&
            (!z[2][0][0] || !z[3][2][0]) &&
            (!z[2][0][0] || !z[4][2][0]) &&
            (!z[2][0][0] || !z[5][2][0]) &&
            (!z[2][1][0] || !z[3][2][0]) &&
            (!z[2][1][0] || !z[4][2][0]) &&
            (!z[2][1][0] || !z[5][2][0]) &&
            (!z[3][2][0] || !z[4][2][0]) &&
            (!z[3][2][0] || !z[5][2][0]) &&
            (!z[4][2][0] || !z[5][2][0])
         )
      ) &&
      (
         (false || x[3][0] || x[3][1] || x[3][2]) ==
         (
            true &&
            (!z[3][0][0] || !z[3][1][0]) &&
            (!z[3][0][0] || !z[3][2][0]) &&
            (!z[3][0][0] || !z[4][3][0]) &&
            (!z[3][0][0] || !z[5][3][0]) &&
            (!z[3][1][0] || !z[3][2][0]) &&
            (!z[3][1][0] || !z[4][3][0]) &&
            (!z[3][1][0] || !z[5][3][0]) &&
            (!z[3][2][0] || !z[4][3][0]) &&
            (!z[3][2][0] || !z[5][3][0]) &&
            (!z[4][3][0] || !z[5][3][0])
         )
      ) &&
      (
         (false || x[4][0] || x[4][1] || x[4][2]) ==
         (
            true &&
            (!z[4][0][0] || !z[4][1][0]) &&
            (!z[4][0][0] || !z[4][2][0]) &&
            (!z[4][0][0] || !z[4][3][0]) &&
            (!z[4][0][0] || !z[5][4][0]) &&
            (!z[4][1][0] || !z[4][2][0]) &&
            (!z[4][1][0] || !z[4][3][0]) &&
            (!z[4][1][0] || !z[5][4][0]) &&
            (!z[4][2][0] || !z[4][3][0]) &&
            (!z[4][2][0] || !z[5][4][0]) &&
            (!z[4][3][0] || !z[5][4][0])
         )
      ) &&
      (
         (false || x[5][0] || x[5][1] || x[5][2]) ==
         (
            true &&
            (!z[5][0][0] || !z[5][1][0]) &&
            (!z[5][0][0] || !z[5][2][0]) &&
            (!z[5][0][0] || !z[5][3][0]) &&
            (!z[5][0][0] || !z[5][4][0]) &&
            (!z[5][1][0] || !z[5][2][0]) &&
            (!z[5][1][0] || !z[5][3][0]) &&
            (!z[5][1][0] || !z[5][4][0]) &&
            (!z[5][2][0] || !z[5][3][0]) &&
            (!z[5][2][0] || !z[5][4][0]) &&
            (!z[5][3][0] || !z[5][4][0])
         )
      )
   ) &&
   (
      true &&
      (false || x[0][0] || x[1][0] || x[2][0] || x[3][0] || x[4][0] || x[5][0]) &&
      (false || x[0][1] || x[1][1] || x[2][1] || x[3][1] || x[4][1] || x[5][1]) &&
      (false || x[0][2] || x[1][2] || x[2][2] || x[3][2] || x[4][2] || x[5][2])
   ) &&
   (
      true &&
      (
         true &&
         (!x[0][0] || !x[1][0]) &&
         (!x[0][0] || !x[2][0]) &&
         (!x[0][0] || !x[3][0]) &&
         (!x[0][0] || !x[4][0]) &&
         (!x[0][0] || !x[5][0]) &&
         (!x[1][0] || !x[2][0]) &&
         (!x[1][0] || !x[3][0]) &&
         (!x[1][0] || !x[4][0]) &&
         (!x[1][0] || !x[5][0]) &&
         (!x[2][0] || !x[3][0]) &&
         (!x[2][0] || !x[4][0]) &&
         (!x[2][0] || !x[5][0]) &&
         (!x[3][0] || !x[4][0]) &&
         (!x[3][0] || !x[5][0]) &&
         (!x[4][0] || !x[5][0])
      ) &&
      (
         true &&
         (!x[0][1] || !x[1][1]) &&
         (!x[0][1] || !x[2][1]) &&
         (!x[0][1] || !x[3][1]) &&
         (!x[0][1] || !x[4][1]) &&
         (!x[0][1] || !x[5][1]) &&
         (!x[1][1] || !x[2][1]) &&
         (!x[1][1] || !x[3][1]) &&
         (!x[1][1] || !x[4][1]) &&
         (!x[1][1] || !x[5][1]) &&
         (!x[2][1] || !x[3][1]) &&
         (!x[2][1] || !x[4][1]) &&
         (!x[2][1] || !x[5][1]) &&
         (!x[3][1] || !x[4][1]) &&
         (!x[3][1] || !x[5][1]) &&
         (!x[4][1] || !x[5][1])
      ) &&
      (
         true &&
         (!x[0][2] || !x[1][2]) &&
         (!x[0][2] || !x[2][2]) &&
         (!x[0][2] || !x[3][2]) &&
         (!x[0][2] || !x[4][2]) &&
         (!x[0][2] || !x[5][2]) &&
         (!x[1][2] || !x[2][2]) &&
         (!x[1][2] || !x[3][2]) &&
         (!x[1][2] || !x[4][2]) &&
         (!x[1][2] || !x[5][2]) &&
         (!x[2][2] || !x[3][2]) &&
         (!x[2][2] || !x[4][2]) &&
         (!x[2][2] || !x[5][2]) &&
         (!x[3][2] || !x[4][2]) &&
         (!x[3][2] || !x[5][2]) &&
         (!x[4][2] || !x[5][2])
      )
   ) &&
   (
      true &&
      (
         true &&
         (!x[0][0] || !x[0][1]) &&
         (!x[0][0] || !x[0][2]) &&
         (!x[0][1] || !x[0][2])
      ) &&
      (
         true &&
         (!x[1][0] || !x[1][1]) &&
         (!x[1][0] || !x[1][2]) &&
         (!x[1][1] || !x[1][2])
      ) &&
      (
         true &&
         (!x[2][0] || !x[2][1]) &&
         (!x[2][0] || !x[2][2]) &&
         (!x[2][1] || !x[2][2])
      ) &&
      (
         true &&
         (!x[3][0] || !x[3][1]) &&
         (!x[3][0] || !x[3][2]) &&
         (!x[3][1] || !x[3][2])
      ) &&
      (
         true &&
         (!x[4][0] || !x[4][1]) &&
         (!x[4][0] || !x[4][2]) &&
         (!x[4][1] || !x[4][2])
      ) &&
      (
         true &&
         (!x[5][0] || !x[5][1]) &&
         (!x[5][0] || !x[5][2]) &&
         (!x[5][1] || !x[5][2])
      )
   )
)

Valuation

Valuation pour le graphe G₂ et la solution pour 3 feuilles :

$ ./k-leafs-cover valuation
Instance :
6 6
1 2
2 3
3 4
0 3
3 5
5 0
3
Valeurs :
5
0 1 2 3 5
Valuation :
   bool y[6][5] = {
         [0][0] = true,
         [1][1] = true,
         [2][2] = true,
         [3][3] = true,
         [5][4] = true,
      }, z[6][6][7] = {
         [1][2][0] = true, [2][1][0] = true,
         [2][3][0] = true, [3][2][0] = true,
         [3][4][0] = true, [4][3][0] = true,
         [0][3][0] = true, [3][0][0] = true,
         [5][0][0] = true, [0][5][0] = true,
         [0][3][1] = true, [3][0][1] = true,
         [0][5][1] = true, [5][0][1] = true,
         [1][2][1] = true, [2][1][1] = true,
         [2][3][1] = true, [3][2][1] = true,
         [3][4][1] = true, [4][3][1] = true,
         [3][5][1] = true, [5][3][1] = true,
         [0][3][2] = true, [3][0][2] = true,
         [0][5][2] = true, [5][0][2] = true,
         [1][2][2] = true, [2][1][2] = true,
         [2][3][2] = true, [3][2][2] = true,
         [3][4][2] = true, [4][3][2] = true,
         [3][5][2] = true, [5][3][2] = true,
         [0][3][3] = true, [3][0][3] = true,
         [0][5][3] = true, [5][0][3] = true,
         [1][2][3] = true, [2][1][3] = true,
         [1][3][3] = true, [3][1][3] = true,
         [2][3][3] = true, [3][2][3] = true,
         [3][4][3] = true, [4][3][3] = true,
         [3][5][3] = true, [5][3][3] = true,
         [0][1][4] = true, [1][0][4] = true,
         [0][2][4] = true, [2][0][4] = true,
         [0][3][4] = true, [3][0][4] = true,
         [0][4][4] = true, [4][0][4] = true,
         [0][5][4] = true, [5][0][4] = true,
         [1][2][4] = true, [2][1][4] = true,
         [1][3][4] = true, [3][1][4] = true,
         [1][4][4] = true, [4][1][4] = true,
         [1][5][4] = true, [5][1][4] = true,
         [2][3][4] = true, [3][2][4] = true,
         [2][4][4] = true, [4][2][4] = true,
         [2][5][4] = true, [5][2][4] = true,
         [3][4][4] = true, [4][3][4] = true,
         [3][5][4] = true, [5][3][4] = true,
         [4][5][4] = true, [5][4][4] = true,
         [0][1][5] = true, [1][0][5] = true,
         [0][2][5] = true, [2][0][5] = true,
         [0][3][5] = true, [3][0][5] = true,
         [0][4][5] = true, [4][0][5] = true,
         [0][5][5] = true, [5][0][5] = true,
         [1][2][5] = true, [2][1][5] = true,
         [1][3][5] = true, [3][1][5] = true,
         [1][4][5] = true, [4][1][5] = true,
         [1][5][5] = true, [5][1][5] = true,
         [2][3][5] = true, [3][2][5] = true,
         [2][4][5] = true, [4][2][5] = true,
         [2][5][5] = true, [5][2][5] = true,
         [3][4][5] = true, [4][3][5] = true,
         [3][5][5] = true, [5][3][5] = true,
         [4][5][5] = true, [5][4][5] = true,
         [0][1][6] = true, [1][0][6] = true,
         [0][2][6] = true, [2][0][6] = true,
         [0][3][6] = true, [3][0][6] = true,
         [0][4][6] = true, [4][0][6] = true,
         [0][5][6] = true, [5][0][6] = true,
         [1][2][6] = true, [2][1][6] = true,
         [1][3][6] = true, [3][1][6] = true,
         [1][4][6] = true, [4][1][6] = true,
         [1][5][6] = true, [5][1][6] = true,
         [2][3][6] = true, [3][2][6] = true,
         [2][4][6] = true, [4][2][6] = true,
         [2][5][6] = true, [5][2][6] = true,
         [3][4][6] = true, [4][3][6] = true,
         [3][5][6] = true, [5][3][6] = true,
         [4][5][6] = true, [5][4][6] = true,
      }, x[6][3] = {
         [1][0] = true,
         [4][1] = true,
         [5][2] = true,
      };

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\nArêtes :");
      for_range (int, edgeNum, 0, < array_len(y), ++) {
         for_array (bool, val, y[edgeNum]) {
            if (val) {
               printf(" %d", edgeNum);
            }
         }
      }
      printf("\n");
   } else {
      printf("Valuation non satisfaisante\n");
   }
}

Votre fichier source pour le solveur SAT devrait avoir ce format :

#include <handymacros.h>

size_t const nbVert = /* nombre de sommets */, nbEdges = /* nombre d’arêtes */, nbWantedLeafs = /* nombre de feuilles exigé */;

bool kLeafsCoverTest(bool y[nbEdges][nbVert - 1], bool z[nbVert][nbVert][nbVert + 1], bool x[nbVert][nbWantedLeafs])
{
   return /* expression */;
}

Cependant, le solveur SAT naïf que j’ai développé est bien trop inefficace pour traiter ce problème. En effet, même avec un graphe de seulement trois sommets et deux arêtes, le nombre de variables est de 46, ce qui correspond à des billions de valuations à tester.

Explications

Le vérificateur et la recherche de solution

Le troisième paramètre de la fonction verify(graph, nbWantedLeafs, selectedEdges) est un sous-ensemble des arêtes du graphe (incarné par un tableau de booléens). Pour vérifier que cela forme bien un arbre, cette fonction vérifie que ce sous-graphe a bien n−1 arêtes (avec n le nombre de sommets), et construit sa liste d’adjacence afin de le parcourir en largeur pour vérifier qu’il est connexe. L’exploration se fait à partir du sommet 0, et chaque sommet est marqué afin de vérifier qu’ils sont tous atteints. Pour vérifier que l’arbre a exactement k arêtes, la fonction compte le nombre de sommets de degré 1 dans la liste d’adjacence.

La fonction findSolution(graph, nbWantedLeafs) utilise le vérificateur, en lui soumettant tous les sous-ensembles de n−1 arêtes, jusqu’à en trouver un qui soit accepté.

L’algorithme de réduction vers SAT

L’algorithme à compléter au DS demandait d’utiliser les trois grands tableaux de booléens suivants :

y_e,j : le sous-ensemble des arêtes sélectionnées, qui doivent correspondre à l’arbre couvrant à k feuilles (0 ⩽ j < n−1) ;
z_u,u’,v : l’existence d’un chemin entre deux sommets u et u’, en n’utilisant que des arêtes du sous-ensemble (représenté par les y_e,j), et sans passer par un sommet de numéro supérieur ou égal à v (0 ⩽ v ⩽ n) ;
x_v,i : l’ensemble des k feuilles (0 ⩽ i < k).

Note : les conventions de mon algorithme diffèrent un peu de celles du DS. Dans le sujet du DS, les sommets et les positions étaient numérotés à partir de 1, et dans la notation z_u,u’,v, le sommet v était inclus comme sommet intermédiaire possible. Mon algorithme considère que les numérotations commencent à zéro et que le sommet v n’est pas inclus, conventions un peu plus courantes en programmation.

Le sens de ces variables n’est bien sûr pas acquis d’avance, et l’objectif de la formule est de le contraindre, puis de s’en servir pour assurer que les arêtes sélectionnées forment bien un arbre couvrant qui n’a pas plus de k feuilles. La fonction reduceToSat(graph, nbWantedLeafs) produit le code pour trois contraintes φ1, φ2 et φ3 (les mêmes que dans le sujet du DS) : une pour chaque grand tableau, en connectant ce dernier avec le tableau précédent.

φ1 et φ3 utilisent la fonction constrainSatSet(name, superSize, size) qui code les trois contraintes assurant que le tableau name est bien un sous-ensemble de taille size d’un ensemble de taille superSize ; il s’agit du même tryptique « au moins un par position, au plus un par position, au plus une position pour un », déjà utilisé pour la réduction du problème Couverture par sommets. φ1 ne contient d’ailleurs rien d’autre que ça.

S’agissant de z_u,u’,v, il faut remarquer que :

z_u,u’,0 indique si u et u’ sont voisins dans le sous-graphe, l’arête correspondante est alors la paire {u,u’}, et si cette arête n’existe pas dans le graphe alors y_{u,u’},j n’existe pas non plus et donc est toujours considéré comme faux ;
z_u,u’,n indique s’il y a un chemin entre u et u’ dans le sous-graphe (sans contrainte).

φ2 est divisé en trois contraintes :

z_u,u’,0 ⇔ y_{u,u’},j pour un certain j (deux sommets sont voisins si et seulement si une arête les relie dans le sous-graphe) ;
z_u,u’,v+1 pour v de 0 à n−1 ⇔ z_u,u’,v ou (z_u,v,v et z_u’,v,v) (deux sommets sont accessibles avec les v+1 premiers sommets s’ils l’étaient déjà sans le sommet v ou si rajouter le sommet v permet de les relier) ;
tous les z_u,u’,n sont vrais (sinon le sous-graphe n’est pas un arbre et n’est donc pas connexe).

Le « si et seulement si » est codé par == en C.

Enfin, dans φ3, il faut vérifier que chaque sommet de l’ensemble des feuilles a bien un seul voisin, et réciproquement. Pour vérifier si un sommet n’a qu’un seul voisin, on teste toute les paires {z_u,u₁,0, z_u,u₂,0} : il ne doit pas y en avoir deux vrais à la fois. Encore une fois, l’opérateur C == est utilisé : un sommet est dans l’ensemble des feuilles si et seulement si il n’a pas plus d’un voisin. Cette contrainte est la première grande parenthèse de φ3, suivie par les contraintes de constrainSatSet.

La génération de valuation

Ce mode ne prend en entrée que l’instance (graphe et nombre de feuilles voulu) et le certificat (sous-ensemble d’arêtes).

Pour générer le tableau z_u,u’,v, l’algorithme de Warshall est employé, pour transformer progressivement la matrice d’adjacence du sous-graphe en matrice d’accessibilité.

Pour générer le tableau x_v,i, les degrés sont calculés et les sommets de degré 1 sont ajoutés comme feuilles. Notez que s’il y a plus de k sommets de degré 1, alors certaines feuilles seront aux mêmes positions i afin que le code C demeure valide.