Un système linéaire pour une variante de SAT

Bon, j'explique un peu en partant du problème 3-SAT que tout le monde connait ici je pense

1) Ce problème se réduit à ONE-IN-THREE-SAT en remplaçant chaque clause $C=(x\vee y\vee z)$ par $3$ ensembles :
$$(\lnot x,a,b),(y,b,c),(\lnot z,c,d)$$
où $a,b,c,d$ sont des nouvelles variables spécifiques à $C$.
Le nouveau problème consiste à décider si chaque ensemble peut contenir exactement un littéral vrai.

2) On peut ensuite éliminer les négations en introduisant pour chaque variable $x$ un ensemble $(x,x')$ où $x'$ est une nouvelle variable et en remplaçant tous les $\lnot x$ par $x'$.

3) Pour ce nouveau problème que je nomme ONE-SAT dans le papier, je formule des conditions nécessaires en termes d'équations linéaires.
On pourrait être tenté de travailler sur $Z/2Z$ mais alors $1+1+1=1$ fait que cela ne correspond plus au problème. Les solutions pour un ensemble à deux éléments sont $(0,1)$ ou $(1,0)$ et à trois éléments sont $(0,0,1),(0,1,0),(1,0,0)$ et pas $(1,1,1)$.

4) Du coup on obtient des premières relations du style $x+y+z=1$ pour un ensemble $(x,y,z)$.

5) Pour éviter d'avoir des multiplications, je code le produit $x_i.x_j$ par une nouvelle variable $x_{i,j}$. Pour $x_i$ et $x_j$ différents et dans le même ensemble, on a forcément $x_{i,j}=0$.

6) Les autres relations sont des traductions du fait que pour un ensemble $(x_a,x_b,x_c)$ on a
$$x_i=x_i.1=x_i.(x_a+x_b+x_c)=x_{i,a}+x_{i,b}+x_{i,c}$$

7) La méthode de résolution du système me semble suffisante.
Elle prend en compte le fait que si $x+y+z=0$ alors nécessairement $x=y=z=0$.
C'est une façon polynomiale de faire de la résolution d'équation linéaires en supposant toutes les variables positives.
C'est tout ce que j'ai trouvé comme méthode...mais peut-être qu'il y a mieux...mais il faut rester polynomial en temps.

Oui je connais ton point de vue et tes doutes et n'espère plus convaincre quiconque que P=NP

Je vais désormais me contenter de proposer des méthodes très simples qui "marchent" sur les cas testés...jusqu'à preuve du contraire.

C'est applicatif et pragmatique....et ça m'occupe.