SAT Solver with Monte Carlo
                                                                  Wild El Khadra ( wildelkhadra@gmx.fr)

Abstract. We describe a new algorithm to solve a 3SAT problem with the Monte Carlo method.

KeyWords :3SAT , Monte Carlo.volume calculation

 
1) Introduction:

L'objectif de cette étude est de présenter un algorithme pour résoudre le problème 3SAT et une implémentation en c# de cet algorithme.

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 notera les clauses d'un système 3SAT (x,y,z) =1.

On peut traduire une clause valide (x,y,z)=1 en un nouveau système relaxé sur les réels:

0<= x <=1 , 0<= y<=1 , 0<= z <=1 ,x+y+z >=1 (*)

Si on a une variable négative on la remplace par 1-x dans x+y+z>=1.

A un système 3sat ( qui dépend des variables x1...........xn) on associe donc un nouveau problème d(optimisation linéaire .

Pour se ramaner à une solution binaire on joute deux contraintes

pour 1<=p<=n

x1+........xn=p

et

x1 * x1 ..........xn*xn=p

2) Algorithme:

On note N le nombre des variables du système.

Pour chaque entier p entre 1 et N

Si on considère une instance d'un problème 3SAT.

On lui associé un polyèdre avec les formules (*) .

Pour chaque entier p on ajoute la contrainte ;

                                      x1 +..........................xN <= p .

Si ce nouveau polyèdre croise l'hypersphère x1*x1.........+ xN*xN=p alors la solution est binaire.

On commence par une hypersphère de rayon r > sqrt(p).

Si on désigne par Vp le volume du polyèdre , Vs le volume du l'hypersphère et Vc celui du complément du polyèdre dans l'hypersphère alors

                                     Vs= Vc + Vp

tant que le polyèdre est strictement à l'intérieur de l'hypersphère.

Pour Vs on peut se limiter pour l'hypersphère pour les variables dans  l'hypercube unité.

On peut utiliser une méthode de Monte Carlo pour calculer les trois volumes en question , puis faire baisser le rayon de l'hypersphère pour détecter le moment ou Vs < Vc + Vp.

Si cette valeur seuil est sqrt(p) pour l'une quelconque des valeurs 1<=p<=N alors on a une solution binaire et SAT est valide.

3) Code:

L'implementation est en cours.