SAT having a known solution

                                                                     Wild El Khadra ( wildelkhadra@gmx.fr)

Abstract. We describe a new algorithm to solve a 3SAT problem having a known solution.

KeyWords :3SAT , Known solution .1In3SAT,quadratic equation , linear algebra.

 
1) Introduction:

L'objectif de cette étude est de présenter un algorithme pour résoudre le problème 3SAT ayant déjà une solution connue.

On notera dans la suite !X la variable opposée à X .

On utilisera dans la suite d'une manière indifférente 1 ou True pour la valeur logique positive et 0 ou False pour la valeur négative.

On se donne un système 3SAT qu’on notera (1) dans la suite.

On notera les clauses du système (1)  (x,y,z).

On note Xi les N variables positives du système (1).

On va transformer le système (1) en un autre système 3SAT ayant une solution évidente.

Pour cela on considère le bloc des clauses ayants seulement des variables négatives (!x,!y ,!z).
Pour chacune de ces clauses on introduit N nouvelles clauses ( Xi, !x ,!y, !z) à quatre variables et commençant  par une variable positive Xi.

On peut ramener chacune de ces clauses à 4 variables à deux clauses 3SAT en introduisant une nouvelle variable t  ( Xi,!x ,!t) et (t ,!y, !z).

On concatène les clauses obtenues à partir des clauses négatives du système (1) avec le reste du système (1) (les clauses de ce reste contiennent au moins une variable positive).

Ce nouveau système 3SAT qu’on notera (2) admet une solution évidente (1,...............................1).
Chaque nouvelle solution du système (2)  autre que la solution donnée en haut est une solution du système (1) car elle contient au moins une variable Xi  égale à FALSE et par construction des clauses à quatre variables on doit avoir le bloc négatif valide aussi.

2) Algorithme:

On commence par ordonner les variables dans chaque clause pour avoir une variable positive en place 1 (possible par construction du système (2)):

Ensuite on transforme le système (2) en un système 1In3SAT.

Pour cela on procède de la manière habituelle :

A chaque clause (x,y,z) on associe les trois clauses ( x,b,c) ,(!y,b,a) et (!z,c,d)
ou a,b , c et d sont des nouvelles variables  et x est ici une variable positive.

Comme la solution (1………1)  est une solution de (2), elle nous donne une solution du système 1In3SAT directement : x=1 , b=c=0 et pour a et d cela dépend des signes de y et z.

Une équation 1In3SAT ((x,b,c)=1 a, par construction, la solution évidente (1,0,0) , elle a une autre solution si et seulement si les deux équations suivantes x=b+c et b*c=0 ont une solution non nulle dans l’ensemble des nombres réels.

En effet si par exemple  b*c=0 et b !=0 alors x=b et c=0 o a la solution (0.1,0)  .

Pour le voir on fait le changement de variables xè 1-x

Le système 1In3SAT est ainsi équivalent à une  un système linéaire homogène et un système quadratique à résoudre sur R ( ensemble des réels).

Exemple si on a une clause positive  3SAT ( x,y,z) avec une solution donné (1.1.1).

Le système 1In3SAT est (x,b ;c)=1 , (a, !y,b) =1 et (d , !z,c)=1 dont la solution donnée déduite est

X=y=z=a=d=1 et b=c=0.

Une solution est une solution non toute nulle du système

x=b+c , a=z+b , d=z+c et  b*c=y*b=z*c=0.

On résout le système linéaire homogène par un pivot de) Gauss et on injecte dans le système quadratique, on se retrouve avec p équations quadratiques qui portent sur n variables et  où chacune des équations quadratiques est le produit de deux équations linéaires ( Q= l*K)

L et K sont aussi homogènes.

Rappel ; pour un système linaire homogène AX=0 à n variables on a deux cas possibles

a) Rang(A)=n et donc il y a une seule solution triviale ( 0…….0).

b) rang(A) < n et on a plusieurs solutions possibles.

Pour notre système L1*K1=0, L2*K2=0…………..Lp*Kp=0  on a à distinguer les cas suivants.

1) Si n> p , on peut sélectionner parmi les Li et Ki p équations ( une pour chaque ligne ) et on résolut le sous-système => une solution non nulle.

2) Si n<=p

on va considérer l’espace vectoriel V = { L1…Lp , K1…Kp} et on regarde sa dimension m. on parle de l’espace vectoriel engendré par le système auxiliaire  L1=0,…Lp=0, K1=0…..Kp=0.

a) Si m<n 

on a plusieurs solutions (les 2*p équations Li et Ki sont des combinaisons linéaires de m équations homogènes à n variables ).

b) Si m=n

Pour chaque indice  i = 1….p on forme une base de V qui contient Li  et Ki

V = {Li} + {Ki} + Wi    où {Li} est le vecteur des coefs de Li=0 .

Wi ici est de dimension m-2.

Si {Li} et {Ki} ne sont pas indépendants ( l’un est un multiples de l’autre ) l’équation quadratique devient linéaire et on se ramène à un système à p-1 équations avec n-1 variables.

b.1)  on considère Xi=.{Ki} + Wi   

On teste pour chaque j =1..p et j !=i  si {Lj} ou {Kj} est dans Xi

b.2) on considère Xi= {Li} + Wi   

On teste pour chaque j =1..p et j !=i  si {Lj} ou {Kj} est dans Xi

Si aucun Wi ne vérifie la condition requise dans b alors on a seulement la solution triviale.

L’idée de base ici est de trouver une base ( m vecteurs indépendants ) contenant en même temps un Li et un Ki , il suffit alors d’annuler m-1 équations linéaires ( ou n-1 car m=n ) portants sur n variables.Sinon on a toujours la solution nulle et le système de base  (2) n’admet pas une autre solution et donc (1) est invalide.

4) Complexité:

Les différentes étapes de l'algorithme sont polynomiales , 3SAT est donc P.

5) Code:

 Une implémentation est faite en c# t et est  en cours de tests...

Update 23/06/2025

Ce code est là seulement pour illustrer l'algo et est en cours de debugagge et d'optiimisation.

Simplesolver 1 (3.48 Mo)