Conversion d'un problème KnapSack en SAT

[coinroad]

Bonjour à vous,

J'ai identifié une forme particulière de problème sac à dos qui me semble intéressante pour travailler sur le problème SAT : le problème sac à dos à contrainte disjonctive.

En effet dans un tel problème sac à dos on a une contrainte supplémentaire liée au fait que certains items du sac sont incompatibles entre eux. Du coup on pourrait formaliser un problème N-SAT en mode sac à dos de la façon suivante :

Imaginons un problème 4 SAT avec 4 couples de littéraux (A et -A ; B et -B ; C et -C ; D et -D), et 16 clauses. Nous allons proposer une solution pour traduire les 16 clauses en 8 boites dont le nombre est égal aux 4 couples de littéraux.

A B C D
A B C -D
A B -C D
A B -C -D
A -B C D
A -B C -D
A -B -C D
A -B -C -D
-A B C D
-A B C -D
-A -B C D
-A -B C -D
-A B -C D
-A -B -C D
-A -B -C /
B -C -D /

On a 8 littéraux et 16 clauses.

Si on traduit ce problème en sac à dos à contrainte disjonctive on aura :

En entrée :

On a 8 boites à l'entrée et on doit en retenir seulement 4 dans le sac à dos.
Chaque boite a un poids noté sous forme de lettre positive ou négative (exemple A ou -A)


Chaque boite a une valeur égale à la valeur décimale du rang de toutes les clauses où elle apparaît. Donc plus un littéral apparaît dans un nombre important de clauses et plus sa valeur augmente.

Exemple :
A : 0,1111111100000000
-A : 0,0000000011111110
B : 0,1111000011001001
-B : 0,0000111100110110
C : 0,1100110011110000
-C : 0,0011001100001111
D : 0,1010101010101100
-D : 0,0101010101010001


Intérêt de la conversion des littéraux en boites valuées : Cette approche permet de réduire le nombre de clauses au nombre de littéraux. Cela réduit considérablement la complexité du problème sac à dos en terme de nombre d'items. (Notamment sur les problèmes où le nombre de clauses est très élevé).

En sortie :

On ne doit pas avoir un résultat où figurent des boites incompatibles (par exemple A et -A, B et -B, C et -C , D et -D; E et -E)
L'addition des 4 boites retenues doit produire un résultat dont la valeur est égale à une valeur égale à 0,1111111111111111 (nombre de digits après la virgule * nombre de clauses).


Cette valeur de 0,1111111111111111 est la capacité du sac qui est connue à l'avance car elle est égale au nombre de clauses du cas N-SAT à résoudre.
Dans chaque clause on doit choisir au minimum et au maximum 1 item représenté par la valeur 1.



Cette addition est un peu spéciale, elle n'est pas arithmétique au sens où l’on ne retient qu’une seule valeur positive sur chaque rang décimal pour calculer la valeur totale de la formule.


Le mieux pour faire ce genre d’addition spéciale serait peut-être de recourir au calcul matriciel. On pourrait alors parler d’une somme matricielle des valeurs de rang des différents littéraux.
Ce n’est peut-être même pas un calcul, mais juste une règle d’écriture superposée de plusieurs clauses qui consiste à placer des caractères 1 dans un champ de C digits qui au départ vaut 0.
L’objectif est de remplir totalement le champ de C digits, autrement dit de trouver la formule de N littéraux qui permettra de n’avoir aucun trou et d’obtenir une valeur décimale où il n’y aura que des 1.
Le sac à dos que l'on obtient nous indique donc à la fois si le problème SAT est satisfiable et en plus quelle est la formule (identifiable grâce aux valeurs décimales des 4 boites / littéraux retenus).
Si aucun sac à dos n'est fait c'est que le problème SAT n'est pas satisfiable.

Que pensez-vous d'une telle approche ?
Que proposeriez vous au niveau du code pour gérer d'une façon simple l'incompatibilité des boites de poids opposés ?
Au niveau code, comment traiter la gestion des valeurs des boites et optimiser ce type de somme matricielle un peu particulière qui vise à remplir un champ dont le nombre de caractères est défini à l'avance avec des 1 en ne laissant aucun 0 dans ce champ ?

Je vous remercie pour vos lumières.