SAT2MQ poc en C#
Ce poc en c# est une implémentation de l'algorithme présenté dans From 3SAT TO QP : 3SAT IS P et FROM 3SAT TO MQ
Sat2mq3 (69.91 Ko)
Il est en cours optimisation et de vérification.
update 20/01/2022
Pendant le changement des variables pour s'assurer de l'inversibilité de la matrice , on va la choisir comme 'une matrice triangulaire inférieure avec des 1 sur la diagonale.
Ceci est possible dans un système MQ sous-déterminé.
update 28/05/2022:
L'approche présentée dans la littérature ne semble pas valable en général , en effet la condition Lij=0 ne donne pas forcément une solution du problème MQ.
Si on note n le nombre des variables et m celui des équations.
Une nouvelle approche est de regrouper les termes en Yi ( on utilise y*y=y), après avoir annulé les termes en YiYj on obtient un système MY = B avec tY = (Y1... Ym) M est une combinaison linéaire des YI ; i=m+1...n et B des formes quadratiques des Yi i=m+1...N
On cherche ensuite des Yi, qui rendent M inversible.
Une meilleure approche est de résoudre alternativement le équations Lij=0 pour i>j ou i<j ,
On a ainsi m(m-1)/2 équations à n-m variables .
On détermine la solution générale de ce système qui va dépendre des variables auxiliaires Z1….Zp.
On cherche ensuite si la partie diagonale peut peut-être rendue égale à 1 ( Lii(Z1….Zp)=1 pour i=1…..m
Si on a une solution M est inversible et le système d'origine est SAT
.
Sinon on détermine le rang du système Lii=0 ( celui de la matrice qui le définit ) et on regarde si avec ces valeurs A1…Z on a système MX=B cohérent ( plusieurs solution ) ou pas ( aucune solution).
Ajouter un commentaire