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).