Module projet.solvers.SolverSAT
module pour le solver SAT
Expand source code
""" module pour le solver SAT """
from pysat.formula import CNF
from pysat.solvers import Solver
class SolverSAT :
"""
implementation du solverSAT
"""
def solve(base) :
"""
methode d'appel du solver sur la base de clauses representant le pb traite
:param base: la base de clauses ;
la base est une liste de listes d'entiers non nuls ;
chaque valeur absolue d'un entier correspond a une variable du pb logique ;
si l'entier est positif dans la clause, cela correspond a un literal positif ;
si l'entier est negatif dans la clause, cela correspond a un literal negatif.
:return True si la base de clauses representant le probleme est satisfiable,
False sinon
"""
cnf = CNF(from_clauses = base)
with Solver(bootstrap_with=cnf) as solver:
return solver.solve()
Classes
class SolverSAT
-
implementation du solverSAT
Expand source code
class SolverSAT : """ implementation du solverSAT """ def solve(base) : """ methode d'appel du solver sur la base de clauses representant le pb traite :param base: la base de clauses ; la base est une liste de listes d'entiers non nuls ; chaque valeur absolue d'un entier correspond a une variable du pb logique ; si l'entier est positif dans la clause, cela correspond a un literal positif ; si l'entier est negatif dans la clause, cela correspond a un literal negatif. :return True si la base de clauses representant le probleme est satisfiable, False sinon """ cnf = CNF(from_clauses = base) with Solver(bootstrap_with=cnf) as solver: return solver.solve()
Methods
def solve(base)
-
methode d'appel du solver sur la base de clauses representant le pb traite
:param base: la base de clauses ; la base est une liste de listes d'entiers non nuls ; chaque valeur absolue d'un entier correspond a une variable du pb logique ; si l'entier est positif dans la clause, cela correspond a un literal positif ; si l'entier est negatif dans la clause, cela correspond a un literal negatif.
:return True si la base de clauses representant le probleme est satisfiable, False sinon
Expand source code
def solve(base) : """ methode d'appel du solver sur la base de clauses representant le pb traite :param base: la base de clauses ; la base est une liste de listes d'entiers non nuls ; chaque valeur absolue d'un entier correspond a une variable du pb logique ; si l'entier est positif dans la clause, cela correspond a un literal positif ; si l'entier est negatif dans la clause, cela correspond a un literal negatif. :return True si la base de clauses representant le probleme est satisfiable, False sinon """ cnf = CNF(from_clauses = base) with Solver(bootstrap_with=cnf) as solver: return solver.solve()