From 7e24240ec90ac44a3ba658a338547324a32cd3d4 Mon Sep 17 00:00:00 2001
From: carrote <carrote@etu.univ-grenoble-alpes.fr>
Date: Thu, 14 Apr 2022 22:38:07 +0200
Subject: [PATCH] Ajout sat solveur + modif legeres
---
README.md | 2 +-
sat_3sat.py | 3 +-
satsolveur.py | 86 ++++++++++++++++++++++++++++++++++++++++++++++++
test_sat_3sat.py | 6 ++--
4 files changed, 91 insertions(+), 6 deletions(-)
create mode 100644 satsolveur.py
diff --git a/README.md b/README.md
index a961c8e..f3f9b81 100644
--- a/README.md
+++ b/README.md
@@ -35,7 +35,7 @@ suivit de nz+nu coordonnées de la forme i,j
Pour éxécuter il faut ensuite entrer :
```
-python3 main.py fihcier.tkz [-s]
+python3 main.py [fichier.tkz] [-s]
```
L'option `-s` permet d'écrire les resultat de chaque operation dans des fichiers.
diff --git a/sat_3sat.py b/sat_3sat.py
index 3aefca9..eaa58d9 100644
--- a/sat_3sat.py
+++ b/sat_3sat.py
@@ -106,5 +106,4 @@ class Sat3SAT:
self.clauses_simplifiees,
nom_fichier
)
-
-
+
diff --git a/satsolveur.py b/satsolveur.py
new file mode 100644
index 0000000..eff8bae
--- /dev/null
+++ b/satsolveur.py
@@ -0,0 +1,86 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+"""
+Created on Thu Apr 14 22:15:49 2022
+
+@authors: E. Carrot, L. De Mathan, A. Koshba
+"""
+
+import es_dimacs
+import random
+import math
+
+
+MAX_ITERATION = 1000
+P = 0.5
+
+class SatSolveur:
+ "Programme naif de Sat Solveur"
+
+
+ """
+ Constructeur naïf
+ """
+ def __init__(self, clauses = [], nb_variables = 0):
+ self.nb_variables = nb_variables
+ self.clauses = clauses
+ self.assignation = {}
+
+ """
+ Affecte à l'objet courant l'ensemble de clauses non simplifiée
+ qui se trouvent dans un fichier dimacs
+ """
+ def lireClausesFichier(self, nom_fichier):
+ # On utilise le module es_dimacs
+ u = es_dimacs.lireCNFDimacs(nom_fichier)
+ self.nb_variables = u[0]
+ self.clauses = u[1]
+
+
+ """
+ Fonction principale trouve (ou essaie) un modele à un ensemble de
+ clauses
+ """
+ def lancerSolveur(self):
+ v = self.assignationAleatoire()
+ i = 0
+
+ while not self.estModele() and i < MAX_ITERATION:
+ c = self.choixClauseAleatoire()
+ x = random.random()
+ if x <= P:
+ y = self.choixVariableAleatoire(c)
+ else:
+ y = self.choixVariableDeterministe(c)
+ self.assignation[y] = 1 - self.assignation[y]
+ i++
+
+ if self.estModele():
+ return True
+ else:
+ return False
+
+
+
+ def assignationAleatoire(self):
+ return # TO DO
+
+ def choixClauseAleatoire(self):
+ return # TO DO
+
+ def choixVariableDeterministe(self, clause):
+ return # TO DO
+
+ def choixVariableAleatoire(self, clause):
+ return # TO DO
+
+ def estModele(self):
+ return # TO DO
+
+
+ """
+ Ecrit la dans un fichier en utilisant le format dimacs
+ """
+ def sortieDimacs(self, nom_fichier):
+ # On appelle le module es_dimacs simplement
+ return # TO DO
\ No newline at end of file
diff --git a/test_sat_3sat.py b/test_sat_3sat.py
index 885568b..830b36c 100644
--- a/test_sat_3sat.py
+++ b/test_sat_3sat.py
@@ -10,9 +10,9 @@ from sat_3sat import *
sat3 = Sat3SAT([
[1],
- [-2, 3],
- [-4,5,-6],
- [7,8,9,10,-11,-12,13,14,15]
+ [-3, 2],
+ [-4,6,-5],
+ [7,8,9,15,-11,-12,13,14,10]
], 15)
sat3.conversion()
--
GitLab