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,2In3SAT , regular graphe

 
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 en deux clauses 3SAT avec une nouvelle variables ( 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).

La solution (x=1.......a=1, d=1) est une solution du système 1In3SAT.

L'idée de l'algorithme est de trouver une solution du système 1In3SAT ou l'une des variables x est 0 , cela nous donne une solution du système (2) et donc une solution du système (1).

 Pour chaque variable x du système 1In3SAT on construit l’arbre suivant :la racine est x et les feuilles sont construits suivants le schéma  donné en bas pour une clause simple ( x, b,c).

 Par exemple pour les quatre clauses suivantes (x,b,c) ,(x ,e,f) , ( !y,b,a) et ( !z,c,d) on a le graphe.

Uns fois qu’on a construit l’arbre ayant x comme racine on élague les branches inutiles de la manière suivante :Si un sommet x a un descendant !y et un ascendant y on supprime toute la branche qui commence par x.

Exemple dans l’arbre suivante on supprime les deux branches avec b et c.

Après cette opération l’élagage on vérifie si on a pour chaque branche partant de x au moins un chemin complet, c’est-à-dire une sous branche qui n’a pas subit deux élagages, comme le cas suivant, la branche b est élaguée ( présence de !x ) mais pas cella de droite (c).

Si on a un arbre sans élagage de deux sous branches à chaque branchement on procède à une bi-coloration du graphe en partant de x=0 , celle solution donne une solution au système 1In3SAT sinon on passe à la variable suivante.

A suivre....................

4) Complexité:

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

3) Code: