Gestion de propositions logiques en Python

Je cherche une solution simple

a marqué ce sujet comme résolu.

Bonjour,

Je travaille sur un projet où l’utilisateur doit fournir des propositions logiques très simples à mon programme : (qui représentent la présence ou non de certains éléments dans le résultat final) :

Du type: 

M1 => M2 and M3
M2 and M3 => M4
M1 => M4 xor M5
M2 => M5

où l’on a affaire à des variables booléennes. L’utilisateur peut choisir un seul ou plusieurs des membres de gauche, et les valeurs des autres variables sont déduites du choix de l’utilisateur. Par exemple si l’utilisateur choisit "M2 and M3", M4 sera vraie dans le résultat, et c’est tout ce qui peut être déduit.

Ces propositions doivent être compatibles et ne pas se contredire lorsqu’un seul des membres de gauche est choisi. Je veux vérifier en amont que ce fichier fourni est correct.

Par exemple ci-dessus, si l’utilisateur choisit de mettre M1 à "vrai", il y aura contradiction.

Mais je n’ai pas trouvé de bibliothèque en python permettant de réaliser simplement et en amont cette vérification. Les solutions que j’ai étudiées sont :

  • Interfacer python avec prolog avec pySwip (beaucoup trop lourd ?)
  • Utiliser une bibliothèque comme Kanren … mais qui me paraît beaucoup trop compliquée, mal documentée, et je n’arrive même pas à gérer une simple implication avec.

Connaissez-vous une solution simple ?

Merci d’avance,

+0 -0

Ça me paraît être exactement un problème SAT et je suis sûr qu’il y a plein de bindings vers des solveurs SAT/SMT en Python — ou on peut même en invoquer comme sous-commande en écrivant un fichier qui décrit le problème en entrée.

Voici par exemple les Bindings Python pour z3, avec cet exemple:

p, q = Bools('p q')
demorgan = And(p, q) == Not(Or(Not(p), Not(q)))
print demorgan

def prove(f):
    s = Solver()
    s.add(Not(f))
    if s.check() == unsat:
        print "proved"
    else:
        print "failed to prove"

print "Proving demorgan..."
prove(demorgan)
+3 -0

Intéressant tout ça !

Pour référence la page linker par @gasche ne semble pas être à jour depuis 2ans. Voilà le même code utilisant Python 3.

from z3 import *
import z3

p, q = Bools('p q')
demorgan = And(p, q) == Not(Or(Not(p), Not(q)))

print(demorgan)

def prove(f):
    s = Solver()
    s.add(Not(f))
    if s.check() == unsat:
        print("proved")
    else:
        print("failed to prove")

print("Proving demorgan...")
prove(demorgan)

L’API n’a pas beaucoup évolué il me semble depuis, donc les exemples semblent fonctionné juste en mettant des parenthèses à print.

+1 -0

Remarque au passage: un solveur SAT vérifie qu’un ensemble de contraintes sur des variables booléennes est "satisfiable", c’est-à-dire "pas une contradiction". C’est exactement ce que veut @Michelouzooo. Le bout de code que j’ai montré fait un truc un poil différent, il regarde si l’ensemble de contraintes est "prouvable", donc "une tautologie". C’est plus compliqué que ce qui était demandé — ça se fait en prenant la négation de la formule, et en vérifiant que la négation n’est pas satisfiable.

+3 -0
Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte