Révision de Croyances et Incohérence

Navigation: ← Tweety-3-Advanced-Logics | Index | Tweety-5-Abstract-Argumentation →

Objectifs pédagogiques

  1. Comprendre les principes AGM de révision de croyances
  2. Explorer les mesures d’incohérence sur les bases de connaissances
  3. Maîtriser l’énumération de MUS (Minimal Unsatisfiable Subsets)
  4. Découvrir MaxSAT pour la satisfaction partielle

Prérequis

Exécutez d’abord Tweety-01-Setup-Python.ipynb pour configurer l’environnement JVM.

Durée estimée : 30-40 minutes

# --- Initialisation JVM Tweety + Outils Externes ---
print("--- Verification JVM Tweety + Outils ---")
jvm_ready = False

import jpype
import jpype.imports
import os
import pathlib
import shutil
import platform

# === Configuration COMPLETE des outils externes ===
EXTERNAL_TOOLS = {
    "CLINGO": "",
    "SPASS": "",
    "EPROVER": "",
    "SAT_SOLVER_PYTHON": "",  # Pour pySAT (CaDiCaL, etc.)
    "MARCO": "",              # MUS enumeration
}

def get_tool_path(tool_name):
    """Retourne le chemin valide d'un outil ou None."""
    path_str = EXTERNAL_TOOLS.get(tool_name, "")
    if not path_str: 
        return None
    if shutil.which(path_str):
        return path_str
    path_obj = pathlib.Path(path_str)
    if path_obj.is_file():
        return str(path_obj.resolve())
    if path_obj.is_dir():
        return str(path_obj.resolve())
    return None

# --- Auto-detection des outils ---
system = platform.system()
exe_suffix = ".exe" if system == "Windows" else ""

# 1. Clingo (ASP solver) - Tweety attend le REPERTOIRE
for cp in [shutil.which("clingo"), pathlib.Path(f"ext_tools/clingo/clingo{exe_suffix}"),
           pathlib.Path(f"../ext_tools/clingo/clingo{exe_suffix}")]:
    if cp and (isinstance(cp, str) or cp.exists()):
        parent = pathlib.Path(cp).parent if isinstance(cp, str) else cp.parent
        EXTERNAL_TOOLS["CLINGO"] = str(parent.resolve())
        break

# 2. SPASS (Modal logic prover)
for sp in [shutil.which("SPASS"), pathlib.Path(f"ext_tools/spass/SPASS{exe_suffix}"),
           pathlib.Path(f"../ext_tools/spass/SPASS{exe_suffix}")]:
    if sp and (isinstance(sp, str) or sp.exists()):
        EXTERNAL_TOOLS["SPASS"] = str(pathlib.Path(sp).resolve()) if isinstance(sp, pathlib.Path) else sp
        break

# 3. EProver (FOL theorem prover)
for ep in [shutil.which("eprover"), pathlib.Path(f"../ext_tools/EProver/eprover{exe_suffix}"),
           pathlib.Path(f"ext_tools/EProver/eprover{exe_suffix}")]:
    if ep:
        ep_path = pathlib.Path(ep) if isinstance(ep, str) else ep
        if ep_path.exists():
            EXTERNAL_TOOLS["EPROVER"] = str(ep_path.resolve())
            break

# 4. SAT Solver Python (CaDiCaL, Glucose via pySAT)
for sat in [pathlib.Path("../ext_tools/sat_solver.py"), pathlib.Path("ext_tools/sat_solver.py")]:
    if sat.exists():
        EXTERNAL_TOOLS["SAT_SOLVER_PYTHON"] = str(sat.resolve())
        break

# 5. MARCO (MUS enumerator avec Z3)
for mp in [pathlib.Path("../ext_tools/marco.py"), pathlib.Path("ext_tools/marco.py")]:
    if mp.exists():
        EXTERNAL_TOOLS["MARCO"] = str(mp.resolve())
        break

# === Initialisation JVM ===
if jpype.isJVMStarted():
    print("JVM deja en cours d'execution.")
    jvm_ready = True
else:
    jdk_portable = None
    for jdk_path in [pathlib.Path("jdk-17-portable"), pathlib.Path("../Argument_Analysis/jdk-17-portable")]:
        if jdk_path.exists():
            zulu_dirs = list(jdk_path.glob("zulu*"))
            if zulu_dirs:
                jdk_portable = zulu_dirs[0]
                os.environ["JAVA_HOME"] = str(jdk_portable.resolve())
                print(f"JDK portable: {jdk_portable.name}")
                break
    
    if not os.environ.get("JAVA_HOME"):
        print("ERREUR: JAVA_HOME non defini et JDK portable non trouve.")
    else:
        LIB_DIR = pathlib.Path("libs")
        if not LIB_DIR.exists():
            LIB_DIR = pathlib.Path("../Argument_Analysis/libs")
        
        if LIB_DIR.exists():
            jar_files = list(LIB_DIR.glob("*.jar"))
            if jar_files:
                classpath = os.pathsep.join(str(j.resolve()) for j in jar_files)
                try:
                    jpype.startJVM(classpath=[classpath])
                    print(f"JVM demarree avec {len(jar_files)} JARs.")
                    jvm_ready = True
                except Exception as e:
                    print(f"Erreur demarrage JVM: {e}")

# === Resume des outils ===
if jvm_ready:
    print("\n--- Outils disponibles ---")
    for tool, path in EXTERNAL_TOOLS.items():
        if path:
            short_path = path.split(os.sep)[-1] if len(path) > 30 else path
            print(f"  {tool}: {short_path}")
    print(f"\nJVM prete. Outils: {sum(1 for t,p in EXTERNAL_TOOLS.items() if p)}/{len(EXTERNAL_TOOLS)}")
--- Verification JVM Tweety + Outils ---
JDK portable: zulu17.50.19-ca-jdk17.0.11-win_x64
JVM demarree avec 42 JARs.

--- Outils disponibles ---
  EPROVER: eprover.exe
  SAT_SOLVER_PYTHON: sat_solver.py
  MARCO: marco.py

JVM prete. Outils: 3/5

Environnement opérationnel

L’initialisation ci-dessus a démarré :

JVM Tweety : 42 bibliothèques JAR chargées avec JPype - Logique propositionnelle (PL) - Révision de croyances (CrMas) - Mesures d’incohérence - Solveurs SAT/MaxSAT

Outils externes (détection automatique — voir la sortie ci-dessus) : - CLINGO : Solveur ASP (Answer Set Programming) - SPASS : Prouveur de théorèmes modal - EPROVER : Prouveur FOL - SAT_SOLVER_PYTHON : Solveurs Python (CaDiCaL, Glucose) - MARCO : Énumérateur MUS avec Z3

Note technique : Les outils externes étendent les capacités de Tweety pour des tâches computationnellement intensives. MARCO, par exemple, utilise Z3 pour énumérer les MUS beaucoup plus rapidement que l’algorithme naïf intégré.

Partie 3 : Révision de Croyances et Analyse d’Incohérence

Cette partie aborde des mécanismes de raisonnement plus avancés : comment mettre à jour des croyances face à de nouvelles informations (révision) et comment quantifier ou gérer les contradictions (incohérence). Nous nous concentrerons principalement sur la logique propositionnelle pour ces exemples.

Contexte : Gestion de l’incohérence dans les systèmes intelligents

Dans les systèmes multi-agents ou les bases de connaissances distribuées, les contradictions sont inévitables :

Exemples réels : - Systèmes experts médicaux : Deux diagnostics contradictoires de spécialistes différents - IoT et capteurs : Mesures contradictoires de capteurs de fiabilité variable - Réseaux sociaux : Propagation d’informations contradictoires de sources multiples

Deux approches complémentaires :

Approche But Méthode
Révision de croyances Intégrer de nouvelles informations Suppression minimale, priorités
Mesures d’incohérence Quantifier les contradictions Métriques mathématiques

Cette partie couvre les deux aspects, en commençant par la révision multi-agents.

3.1 Révision de Croyances Multi-Agents (CrMas)

La révision de croyances s’intéresse à l’intégration de nouvelles informations dans une base de connaissances existante, en résolvant les éventuelles contradictions de manière rationnelle (cf. postulats AGM). Tweety implémente notamment des approches pour des bases de croyances multi-agents où chaque information est associée à un agent et où un ordre de crédibilité peut exister entre ces agents.

  • CrMasBeliefSet : Base de croyances multi-agents, nécessite un Order<Agent>.
  • InformationObject : Encapsule une formule et l’agent source.
  • Opérateurs de Révision (org.tweetyproject.beliefdynamics.mas) :
    • CrMasRevisionWrapper: Utilise un opérateur de révision classique (ex: Levi) sur les formules, en ignorant la structure multi-agents sauf pour prioriser la nouvelle information.
    • CrMasSimpleRevisionOperator: Prend en compte la crédibilité des agents de manière simple pour fusionner les informations.
    • CrMasArgumentativeRevisionOperator: Modélise la révision comme un processus argumentatif où les informations des agents plus crédibles peuvent “attaquer” celles des agents moins crédibles.

L’exemple suivant reprend la logique de CrMasExample.java et du TP C#.

# --- 3.1a Test des imports CrMas ---
# NOTE: Cette section utilise des classes qui ont change de package dans Tweety 1.28.
# Les chemins sont corriges pour la version actuelle.

print("--- 3.1a Test des imports CrMas ---")
CrMas_Imports_OK = False

if not jvm_ready:
    print("ERREUR: JVM non demarree.")
else:
    print("Verification des classes CrMas...")
    try:
        import jpype
        from jpype.types import *
        missing_imports = []
        
        # Classes du package beliefdynamics.mas
        for cls_name in ["InformationObject", "CrMasBeliefSet", "CrMasRevisionWrapper"]:
            try:
                jpype.JClass(f"org.tweetyproject.beliefdynamics.mas.{cls_name}")
                print(f"   OK: {cls_name} (from mas)")
            except Exception as e:
                print(f"   FAIL: {cls_name}")
                missing_imports.append(cls_name)
        
        # Classes du package beliefdynamics.operators
        for cls_name in ["CrMasSimpleRevisionOperator", "CrMasArgumentativeRevisionOperator"]:
            try:
                jpype.JClass(f"org.tweetyproject.beliefdynamics.operators.{cls_name}")
                print(f"   OK: {cls_name} (from operators)")
            except Exception as e:
                print(f"   FAIL: {cls_name}")
                missing_imports.append(cls_name)
        
        # Classes du package beliefdynamics (racine)
        for cls_name in ["LeviMultipleBaseRevisionOperator", "DefaultMultipleBaseExpansionOperator"]:
            try:
                jpype.JClass(f"org.tweetyproject.beliefdynamics.{cls_name}")
                print(f"   OK: {cls_name}")
            except Exception as e:
                print(f"   FAIL: {cls_name}")
                missing_imports.append(cls_name)
        
        # Classes kernels
        try:
            jpype.JClass("org.tweetyproject.beliefdynamics.kernels.KernelContractionOperator")
            jpype.JClass("org.tweetyproject.beliefdynamics.kernels.RandomIncisionFunction")
            print("   OK: KernelContractionOperator, RandomIncisionFunction")
        except Exception as e:
            missing_imports.append("KernelClasses")
        
        # Classes agents
        try:
            jpype.JClass("org.tweetyproject.agents.Agent")
            jpype.JClass("org.tweetyproject.agents.DummyAgent")
            jpype.JClass("org.tweetyproject.comparator.Order")
            print("   OK: Agent, DummyAgent, Order")
        except Exception as e:
            missing_imports.append("AgentClasses")
        
        if not missing_imports:
            CrMas_Imports_OK = True
            print("\n==> Tous les imports CrMas reussis!")
        else:
            print(f"\n==> Imports CrMas echoues: {missing_imports}")
            print("    (Normal pour Tweety 1.28+ - API refactorisee)")
    except Exception as e:
        print(f"ERREUR: {e}")

print(f"\nCrMas_Imports_OK = {CrMas_Imports_OK}")
--- 3.1a Test des imports CrMas ---
Verification des classes CrMas...
   OK: InformationObject (from mas)
   OK: CrMasBeliefSet (from mas)
   OK: CrMasRevisionWrapper (from mas)
   OK: CrMasSimpleRevisionOperator (from operators)
   OK: CrMasArgumentativeRevisionOperator (from operators)
   OK: LeviMultipleBaseRevisionOperator
   OK: DefaultMultipleBaseExpansionOperator
   OK: KernelContractionOperator, RandomIncisionFunction
   OK: Agent, DummyAgent, Order

==> Tous les imports CrMas reussis!

CrMas_Imports_OK = True

Initialisation des agents et base de connaissances

Si les imports CrMas sont disponibles, nous pouvons créer:

  1. Des agents avec un ordre de credibilite (A1 > A2 > A3)
  2. Une base de croyances initiale (CrMasBeliefSet)
  3. Des InformationObjects associant une formule a son agent source

L’ordre de credibilite determine quelle information est preferee en cas de conflit.

# --- 3.1b Initialisation agents et base CrMas ---
print("--- 3.1b Initialisation agents et base CrMas ---")

if not CrMas_Imports_OK:
    print("Skipped: imports CrMas non disponibles (Tweety 1.28+ API change).")
else:
    try:
        import jpype
        from jpype.types import *
        from java.util import ArrayList, HashSet, Collection
        
        # Imports classes CrMas
        InformationObject = jpype.JClass("org.tweetyproject.beliefdynamics.mas.InformationObject")
        CrMasBeliefSet = jpype.JClass("org.tweetyproject.beliefdynamics.mas.CrMasBeliefSet")
        DummyAgent = jpype.JClass("org.tweetyproject.agents.DummyAgent")
        Order = jpype.JClass("org.tweetyproject.comparator.Order")
        
        from org.tweetyproject.logics.pl.parser import PlParser
        from org.tweetyproject.logics.pl.syntax import PlFormula, PlSignature
        
        # Classes pour les casts
        PlFormula_class = jpype.JClass("org.tweetyproject.logics.pl.syntax.PlFormula")
        Agent_class = jpype.JClass("org.tweetyproject.agents.Agent")
        Collection_class = jpype.JClass("java.util.Collection")
        
        # Creation des agents
        parser = PlParser()
        agents_list = ArrayList()
        agent1 = DummyAgent("A1")
        agent2 = DummyAgent("A2")
        agent3 = DummyAgent("A3")
        agents_list.add(agent1)
        agents_list.add(agent2)
        agents_list.add(agent3)
        
        # Ordre de credibilite: A1 > A2 > A3
        credOrder = Order(JObject(agents_list, Collection_class))
        credOrder.setOrderedBefore(agent1, agent2)
        credOrder.setOrderedBefore(agent2, agent3)
        print("Ordre de credibilite: A1 > A2 > A3")
        
        # Base de croyances initiale
        pl_sig_empty = PlSignature()
        base = CrMasBeliefSet(credOrder, pl_sig_empty)
        
        # === SCENARIO CONCU POUR DIFFERENCIER SIMPLE vs ARGUMENTATIF ===
        # 
        # Idee: creer des chaines d'attaque ou la propagation argumentative
        # differe de la simple comparaison de credibilite
        #
        # A1 (haute cred): p (fait de base)
        # A2 (moyenne):    q, p=>r (q vrai, si p alors r)
        # A3 (basse):      !q, !r (contredisent A2)
        #
        # Conflits:
        # - A3:!q attaque A2:q -> Simple rejette !q (A2>A3)
        # - A3:!r attaque consequence de A1:p + A2:p=>r
        #   -> Simple: peut garder !r (pas de defenseur direct)
        #   -> Argumentatif: rejette !r car la chaine p + p=>r est defendue
        
        info1 = InformationObject(JObject(parser.parseFormula("p"), PlFormula_class), JObject(agent1, Agent_class))
        info2 = InformationObject(JObject(parser.parseFormula("q"), PlFormula_class), JObject(agent2, Agent_class))
        info3 = InformationObject(JObject(parser.parseFormula("p=>r"), PlFormula_class), JObject(agent2, Agent_class))
        info4 = InformationObject(JObject(parser.parseFormula("!q"), PlFormula_class), JObject(agent3, Agent_class))
        info5 = InformationObject(JObject(parser.parseFormula("!r"), PlFormula_class), JObject(agent3, Agent_class))
        
        base.add(info1)
        base.add(info2)
        base.add(info3)
        base.add(info4)
        base.add(info5)
        print(f"\nBase initiale: {base}")
        print("  A1:p, A2:q, A2:(p=>r), A3:!q, A3:!r")
        
        # Nouvelles informations: A2 revise avec !p, A3 ajoute s
        # !p de A2 attaque p de A1, mais A1 plus credible
        news_collection = HashSet()
        news_collection.add(InformationObject(JObject(parser.parseFormula("!p"), PlFormula_class), JObject(agent2, Agent_class)))
        news_collection.add(InformationObject(JObject(parser.parseFormula("s"), PlFormula_class), JObject(agent3, Agent_class)))
        news_str = ", ".join([str(info.getFormula())+" ("+str(info.getSource().getName())+")" for info in news_collection])
        print(f"\nNouvelles infos: {{ {news_str} }}")
        print("  A2:!p contredit A1:p (A1 plus credible)")
        print("  A3:s nouvelle info neutre")
        
        print("\n==> Base et news prets pour la revision.")
    except Exception as e:
        print(f"ERREUR initialisation: {e}")
        import traceback
        traceback.print_exc()
--- 3.1b Initialisation agents et base CrMas ---
Ordre de credibilite: A1 > A2 > A3

Base initiale: { A1:p, A2:(p=>r), A3:!q, A3:!r, A2:q }
  A1:p, A2:q, A2:(p=>r), A3:!q, A3:!r

Nouvelles infos: { !p (A2), s (A3) }
  A2:!p contredit A1:p (A1 plus credible)
  A3:s nouvelle info neutre

==> Base et news prets pour la revision.

La théorie AGM : postulats et triade du changement de croyance

La théorie AGM (Alchurrón, Gärdenfors & Makinson — On the Logic of Theory Change, 1985) ne définit pas des « opérateurs » : elle formalise comment un agent rationnel fait évoluer sa base de croyances \(K\) (un ensemble clos par conséquence logique) face à une nouvelle information. Elle pose une triade d’opérations et une liste de postulats que ces opérations doivent satisfaire pour être « rationnelles ».

La triade AGM. Soit \(K\) la base de croyances et \(A\) la nouvelle formule :

Opération Notation Définition
Expansion \(K + A\) Ajouter \(A\) à \(K\) et fermer par déduction (sans rien retirer). Peut rendre \(K\) incohérent.
Contraction \(K - A\) Retirer \(A\) de \(K\) de façon minimale (sans rien ajouter), en préservant la cohérence.
Révision \(K * A\) Intégrer \(A\) prioritairement, en retirant le strict minimum pour rester cohérent.

Les postulats AGM. La révision \(K*A\) doit satisfaire 8 postulats (clôture, succès — \(A \in K*A\) ; inclusion ; vacuité ; préservation de la cohérence ; extensionnalité ; et les deux postulats de sur/sous-expansion liés à la conjonction) ; la contraction \(K-A\) en satisfait 6 (les duaux, plus Recovery : \(K \subseteq (K-A)+A\)). Ces postulats contraignent le changement à être minimal et cohérent. Aucun ne s’appelle « Levi », « Simple » ou « Argumentatif ».

Les identités de construction. Révision et contraction ne sont pas indépendantes : chacune se construit à partir de l’autre.

  • Identité de Levi : \(\quad K * A \;=\; (K - \neg A) + A\) — réviser par \(A\), c’est contracter \(\neg A\) puis expanser \(A\).
  • Identité de Harper : \(\quad K - A \;=\; K \,\cap\, (K * \neg A)\) — contracter \(A\), c’est intersecter \(K\) avec la révision par \(\neg A\) (duale de Levi).

À ne pas confondre. Les trois opérateurs exécutés ci-dessous (Levi, Simple, Argumentatif) sont des implémentations concrètes de la bibliothèque Tweety (modules beliefdynamics + CrMas multi-agents) qui réalisent une révision. L’« opérateur Levi » de Tweety enchaîne littéralement contraction puis expansion — c’est l’identité de Levi ci-dessus codée telle quelle. Ce ne sont pas des postulats AGM : les postulats sont les contraintes rationnelles que ces opérateurs s’efforcent de respecter.

# --- 3.1c Operateurs de revision CrMas ---
print("--- 3.1c Operateurs de revision CrMas ---")

if not CrMas_Imports_OK:
    print("Skipped: imports CrMas non disponibles (Tweety 1.28+ API change).")
else:
    try:
        import jpype
        from jpype.types import *
        
        # Imports des operateurs
        CrMasRevisionWrapper = jpype.JClass("org.tweetyproject.beliefdynamics.mas.CrMasRevisionWrapper")
        CrMasSimpleRevisionOperator = jpype.JClass("org.tweetyproject.beliefdynamics.operators.CrMasSimpleRevisionOperator")
        CrMasArgumentativeRevisionOperator = jpype.JClass("org.tweetyproject.beliefdynamics.operators.CrMasArgumentativeRevisionOperator")
        LeviMultipleBaseRevisionOperator = jpype.JClass("org.tweetyproject.beliefdynamics.LeviMultipleBaseRevisionOperator")
        DefaultMultipleBaseExpansionOperator = jpype.JClass("org.tweetyproject.beliefdynamics.DefaultMultipleBaseExpansionOperator")
        KernelContractionOperator = jpype.JClass("org.tweetyproject.beliefdynamics.kernels.KernelContractionOperator")
        RandomIncisionFunction = jpype.JClass("org.tweetyproject.beliefdynamics.kernels.RandomIncisionFunction")
        
        from org.tweetyproject.logics.pl.reasoner import SimplePlReasoner
        KernelProvider_class = jpype.JClass("org.tweetyproject.commons.KernelProvider")
        Collection_class = jpype.JClass("java.util.Collection")
        
        print(f"Revision de: {base}")
        print(f"Avec: {{ {news_str} }}")
        print()
        
        # 1) Operateur Levi (prioritaire)
        print("1. Operateur Levi (prioritaire):")
        try:
            incision_func = RandomIncisionFunction()
            pl_reasoner_instance = SimplePlReasoner()
            kernel_contract = KernelContractionOperator(incision_func, JObject(pl_reasoner_instance, KernelProvider_class))
            levi_operator = LeviMultipleBaseRevisionOperator(kernel_contract, DefaultMultipleBaseExpansionOperator())
            revision_prio = CrMasRevisionWrapper(levi_operator)
            result_prio = revision_prio.revise(base, JObject(news_collection, Collection_class))
            print(f"   Resultat: {result_prio}")
        except Exception as e:
            print(f"   Erreur: {e}")
        
        # 2) Operateur Simple (credibilite)
        print("\n2. Operateur Simple (credibilite):")
        try:
            revision_simple = CrMasSimpleRevisionOperator()
            result_simple = revision_simple.revise(base, JObject(news_collection, Collection_class))
            print(f"   Resultat: {result_simple}")
        except Exception as e:
            print(f"   Erreur: {e}")
        
        # 3) Operateur Argumentatif (credibilite + argumentation)
        print("\n3. Operateur Argumentatif (argumentation):")
        try:
            revision_arg = CrMasArgumentativeRevisionOperator()
            result_arg = revision_arg.revise(base, JObject(news_collection, Collection_class))
            print(f"   Resultat: {result_arg}")
        except Exception as e:
            print(f"   Erreur: {e}")
        
        print("\n==> Comparaison des 3 operateurs terminee.")
    except Exception as e:
        print(f"ERREUR operateurs: {e}")
        import traceback
        traceback.print_exc()
--- 3.1c Operateurs de revision CrMas ---
Revision de: { A1:p, A2:(p=>r), A3:!q, A3:!r, A2:q }
Avec: { !p (A2), s (A3) }

1. Operateur Levi (prioritaire):
   Resultat: [A2:!p, A1:p, A3:!r, A2:q, A3:s]

2. Operateur Simple (credibilite):
   Resultat: [A1:p, A2:(p=>r), A3:!q, A3:!r, A2:q]

3. Operateur Argumentatif (argumentation):
   Resultat: [A1:p, A3:!r, A2:q, A3:s]

==> Comparaison des 3 operateurs terminee.

Lecture AGM du code : noyaux, fonction d’incision et enracinement

Le code ci-dessus met en œuvre les briques AGM « de bas niveau ». Repérons-les dans ce que Tweety vient d’exécuter.

Contraction par noyaux (kernel contraction). La ligne LeviMultipleBaseRevisionOperator(kernel_contract, DefaultMultipleBaseExpansionOperator()) applique littéralement l’identité de Levi \(K*A = (K-\neg A)+A\) : elle contracte via kernel_contract puis expansent via DefaultMultipleBaseExpansionOperator. La contraction KernelContractionOperator repose sur deux notions AGM (Hansson, 1994) :

  • Un noyau (kernel) de \(K\) relativement à \(A\) est un sous-ensemble minimal de \(K\) qui, uni à \(A\), devient incohérent — un « point de conflit » minimal. L’opérateur calcule tous les noyaux.
  • La fonction d’incision (incision function, ici RandomIncisionFunction) choisit, dans chaque noyau, quelles formules sacrifier pour rétablir la cohérence, en coupant au plus juste. Une incision rationnelle est sélective (minimalité du changement) ; l’implémentation aléatoire de Tweety est un démonstrateur, pas une politique optimale.
  • La notion duale est l’ensemble restant (remainder set) : les sous-ensembles maximaux de \(K\) restant cohérents avec \(A\). Contraction par noyaux et contraction par ensembles restants sont deux routes équivalentes vers un même résultat AGM.

Enracinement épistémique (epistemic entrenchment) — à ne pas confondre avec la crédibilité. Gärdenfors & Makinson (1988) montrent que toute contraction respectant les postulats AGM est caractérisée par un ordre d’enracinement \(\leq_E\) sur les croyances : \(A \leq_E B\) signifie « l’agent renonce plus volontiers à \(A\) qu’à \(B\) ». Le théorème de représentation relie cet ordre à la contraction — on retire en priorité les croyances les moins enracinées. Cet ordre porte sur les croyances elles-mêmes.

Or le notebook introduit par ailleurs un ordre de crédibilité Order<Agent> (A1 > A2 > A3, cellule précédente). Les deux ordres sont orthogonaux :

Enracinement épistémique \(\leq_E\) Crédibilité Order<Agent>
Porte sur les croyances (formules) les sources (agents)
Question « à quoi renoncer pour rester cohérent ? » « qui croire quand deux sources se contredisent ? »
Utilisé par contraction AGM (mono-agent) opérateurs CrMas Simple / Argumentatif (multi-agents)

Une source très crédible peut énoncer une croyance périphérique (faible enracinement) : les deux classements ne se déduisent pas l’un de l’autre. Les opérateurs Simple et Argumentatif ci-dessus raisonnent en crédibilité (multi-agents) ; l’opérateur Levi, via la contraction par noyaux, relève du courant AGM mono-agent (enracinement). Le notebook navigue ainsi entre deux familles de la révision de croyances.

À noter. Les sections suivantes (3.2–3.4 : mesures d’incohérence, MUS, MaxSAT) ne révisent plus l’incohérence : elles la mesurent et la diagnostiquent. C’est un courant de recherche complémentaire, distinct de la révision AGM — mais tout aussi utile pour décider quoi réviser.

Interpretation des résultats de revision

Les trois opérateurs produisent des résultats différents selon leur stratégie de gestion des conflits :

Scénario concu pour differencier les opérateurs :

Agent Formule Rôle
A1 (haute) p Fait de base
A2 (moyenne) q, p=>r Faits + implication
A3 (basse) !q, !r Contradictions

Nouvelles infos : !p (A2), s (A3)

Analyse des conflits :

  1. A3:!q vs A2:q : Conflit direct, A2 > A3
  2. A3:!r vs (A1:p + A2:p=>r) : Conflit indirect via deduction
  3. A2:!p vs A1:p : A1 > A2, donc !p rejete

Comportement observé (cf. sorties committées ci-dessus) :

Opérateur Résultat Intègre !p (A2) ? Intègre s (A3) ? !r ?
Levi 5 formules Oui Oui Garde
Simple base initiale (5) Non Non Garde
Argumentatif 4 formules Non Oui Garde

Les trois opérateurs gardent !r : aucun ne rejette ici la contradiction directe de r émise par A3. La différence entre les opérateurs ne porte donc pas sur !r (contrairement à l’intuition du scénario), mais sur quelles nouvelles informations ils intègrent :

  • Levi (révision prioritaire par contraction de noyaux) intègre les deux nouvelles infos (!p et s) : la nouvelle information prime, quitte à écarter p=>r et !q pour préserver la cohérence.
  • Simple (comparaison de crédibilité pure) n’en intègre aucune : !p et s viennent d’agents moins crédibles (A2, A3) que le détenteur de p (A1), donc la base reste inchangée.
  • Argumentatif intègre s (info neutre de A3) mais pas !p (qui contredirait p de A1, l’agent le plus crédible), et retire en prime p=>r et !q.

Honnêteté sur l’objectif initial. Le scénario (commentaire de la cellule de définition) visait à faire ressortir une différence de traitement de !r entre Simple et Argumentatif. La sortie réelle de Tweety 1.28+ ne le confirme pas : les deux gardent !r. Plutôt que de forcer la narration attendue (ce serait malhonnête vis-à-vis de la sortie committée), on retient la différence réellement observée — la stratégie d’intégration des nouvelles informations — qui n’en reste pas moins pédagogiquement riche (priorité Levi vs crédibilité Simple vs raisonnement Argumentatif).

3.2 Mesures d’Incohérence (PL)

Mesurer le degré d’incohérence d’une base de connaissances propositionnelle.

  • ContensionInconsistencyMeasure: Basée sur le nombre minimal de variables à assigner pour trouver un modèle.
  • MaInconsistencyMeasure / McscInconsistencyMeasure: Basées sur les MUS (Minimal Unsatisfiable Subsets). Nécessitent un énumérateur de MUS (ex: MarcoMusEnumerator externe ou NaiveMusEnumerator interne).
  • FuzzyInconsistencyMeasure: Utilise une sémantique floue pour évaluer la satisfaction des formules.
  • DSum/DMax/DHitInconsistencyMeasure: Basées sur la distance (ex: distance de Dalal) entre la base et les mondes possibles les plus proches la satisfaisant.

Transition : De la révision aux mesures d’incohérence

La section précédente (CrMas) a montré comment résoudre les contradictions en choisissant quelles formules conserver. Mais avant de réviser, il est souvent utile de quantifier le degré d’incohérence.

Pourquoi mesurer l’incohérence ?

  1. Diagnostic : Identifier les zones problématiques d’une base de connaissances
  2. Priorisation : Décider quelles parties réviser en premier
  3. Comparaison : Évaluer la qualité de différentes bases de connaissances
  4. Seuillage : Déclencher une révision uniquement si l’incohérence dépasse un seuil

Approches principales : - Contension : Combien de variables minimalement problématiques - Distance : Proximité aux mondes possibles cohérents - MUS : Nombre de conflits minimaux irréductibles

Les exemples ci-dessous illustrent chaque famille de mesures.

# --- 3.2 Mesures d'Incoherence (PL) ---
# NOTE: PlParser est dans org.tweetyproject.logics.pl.parser (pas .syntax)
# Les mesures de distance ont ete renommees en Tweety 1.28:
#   - DSumInconsistencyMeasure -> DSumSatInconsistencyMeasure
#   - DMaxInconsistencyMeasure -> DMaxSatInconsistencyMeasure
#   - DHitInconsistencyMeasure -> DHitSatInconsistencyMeasure
# Ma/Mcsc sont dans org.tweetyproject.logics.commons.analysis
# FuzzyInconsistencyMeasure necessite un solveur non-lineaire (non disponible par defaut)

print("\n--- 3.2 Mesures d'Incoherence (PL) ---")

if not jvm_ready:
    print("ERREUR: JVM non demarree.")
else:
    print("JVM prete. Execution des exemples de mesures d'incoherence...")
    try:
        import jpype
        from jpype.types import *

        # Imports PL de base - PlParser est dans .parser, pas .syntax!
        from org.tweetyproject.logics.pl.parser import PlParser
        from org.tweetyproject.logics.pl.syntax import PlBeliefSet, PlFormula, PlSignature
        from org.tweetyproject.logics.pl.sat import Sat4jSolver, SatSolver
        from java.util import Collection
        print("   OK: Imports PL de base (PlParser from .parser)")

        # Imports pour le solveur d'optimisation
        from org.tweetyproject.math.opt.solver import Solver, ApacheCommonsSimplex
        Solver.setDefaultGeneralSolver(ApacheCommonsSimplex())
        print("   OK: Solveur d'optimisation configure (ApacheCommonsSimplex)")

        # Imports specifiques aux mesures
        from org.tweetyproject.logics.pl.analysis import ContensionInconsistencyMeasure
        # Note: DSum/DMax/DHit renommes en *Sat* dans Tweety 1.28
        from org.tweetyproject.logics.pl.analysis import DSumSatInconsistencyMeasure, DMaxSatInconsistencyMeasure, DHitSatInconsistencyMeasure
        from org.tweetyproject.logics.commons.analysis import NaiveMusEnumerator
        # Ma/Mcsc sont dans commons.analysis
        from org.tweetyproject.logics.commons.analysis import MaInconsistencyMeasure, McscInconsistencyMeasure

        print("   OK: Tous les imports pour Mesures d'Incoherence reussis.")

        # Classe pour cast
        Collection_class = jpype.JClass("java.util.Collection")

        # --- Configuration ---
        parser_inc = PlParser()
        SatSolver.setDefaultSolver(Sat4jSolver())

        # --- Exemples ---

        # 1. Contension (Base sur ContensionExample.java)
        print("\n--- Mesure Contension ---")
        kb_cont = PlBeliefSet()
        formulas_cont = ["a", "!a && b", "!b", "c || a", "!c || a", "!c || d", "!d", "d", "c"]
        for f_str in formulas_cont: kb_cont.add(parser_inc.parseFormula(f_str))
        print(f"KB: {kb_cont}")
        try:
            cont_measure = ContensionInconsistencyMeasure()
            # Cast en Collection pour eviter ambiguite JPype
            cont_value = cont_measure.inconsistencyMeasure(JObject(kb_cont, Collection_class))
            print(f"Valeur Contension: {cont_value}")
        except Exception as e_cont:
            print(f"Erreur Contension: {e_cont}")

        # 2. DSum / DMax / DHit (mesures basees sur distance de Dalal)
        print("\n--- Mesures Basees sur Distance (Dalal) ---")
        kb_dist = PlBeliefSet()
        kb_dist.add(parser_inc.parseFormula("a && b && c"))
        kb_dist.add(parser_inc.parseFormula("!a && !b && !c"))
        print(f"KB pour Distance: {kb_dist}")
        try:
            dsum_measure = DSumSatInconsistencyMeasure()
            dsum_value = dsum_measure.inconsistencyMeasure(JObject(kb_dist, Collection_class))
            print(f"Valeur DSum (Sat): {dsum_value}")

            dmax_measure = DMaxSatInconsistencyMeasure()
            dmax_value = dmax_measure.inconsistencyMeasure(JObject(kb_dist, Collection_class))
            print(f"Valeur DMax (Sat): {dmax_value}")

            dhit_measure = DHitSatInconsistencyMeasure()
            dhit_value = dhit_measure.inconsistencyMeasure(JObject(kb_dist, Collection_class))
            print(f"Valeur DHit (Sat): {dhit_value}")
        except jpype.JException as e_dist_java:
             print(f"Erreur Java (Mesures Distance): {e_dist_java.message()}")
        except Exception as e_dist_py:
             print(f"Erreur Python (Mesures Distance): {e_dist_py}")

        # 3. Mesures Ma et Mcsc (basees sur MUS)
        print("\n--- Mesures Ma / Mcsc (basees sur MUS) ---")
        kb_mus_demo = PlBeliefSet()
        formulas_mus_demo = ["a", "!a", "!a && !b", "b"]
        for f_str in formulas_mus_demo: kb_mus_demo.add(parser_inc.parseFormula(f_str))
        print(f"KB pour Ma/Mcsc: {kb_mus_demo}")
        try:
            mus_enum_naive = NaiveMusEnumerator(SatSolver.getDefaultSolver())
            ma_measure_naive = MaInconsistencyMeasure(mus_enum_naive)
            ma_value = ma_measure_naive.inconsistencyMeasure(JObject(kb_mus_demo, Collection_class))
            print(f"Valeur Ma (Naive): {ma_value}")

            mcsc_measure_naive = McscInconsistencyMeasure(mus_enum_naive)
            mcsc_value = mcsc_measure_naive.inconsistencyMeasure(JObject(kb_mus_demo, Collection_class))
            print(f"Valeur Mcsc (Naive): {mcsc_value}")
        except Exception as e_ma_mcsc:
             print(f"Erreur calcul Ma/Mcsc (Naive): {e_ma_mcsc}")

        # Note: FuzzyInconsistencyMeasure necessite un solveur non-lineaire
        print("\n--- Note: FuzzyInconsistencyMeasure ---")
        print("FuzzyInconsistencyMeasure necessite un solveur d'optimisation non-lineaire")
        print("(pas disponible par defaut). Omis dans cet exemple.")

    except ImportError as e:
        print(f"Erreur d'import pour Mesures d'Incoherence : {e}")
    except jpype.JException as e_java:
        print(f"Erreur Java generale dans Mesures d'Incoherence: {e_java.message()}")
    except Exception as e_gen:
        print(f"Erreur Python inattendue dans Mesures d'Incoherence: {e_gen}")
        import traceback; traceback.print_exc()

--- 3.2 Mesures d'Incoherence (PL) ---
JVM prete. Execution des exemples de mesures d'incoherence...
   OK: Imports PL de base (PlParser from .parser)
   OK: Solveur d'optimisation configure (ApacheCommonsSimplex)
   OK: Tous les imports pour Mesures d'Incoherence reussis.

--- Mesure Contension ---
KB: { !a&&b, !c||d, a, !b, !d, c, d, c||a, !c||a }
Valeur Contension: 3.0

--- Mesures Basees sur Distance (Dalal) ---
KB pour Distance: { a&&b&&c, !a&&!b&&!c }
Valeur DSum (Sat): 3.0
Valeur DMax (Sat): 2.0
Valeur DHit (Sat): 1.0

--- Mesures Ma / Mcsc (basees sur MUS) ---
KB pour Ma/Mcsc: { !a&&!b, !a, a, b }
Valeur Ma (Naive): 2.0
Valeur Mcsc (Naive): 4.0

--- Note: FuzzyInconsistencyMeasure ---
FuzzyInconsistencyMeasure necessite un solveur d'optimisation non-lineaire
(pas disponible par defaut). Omis dans cet exemple.

Interpretation des mesures d’incoherence

Les valeurs ci-dessus quantifient le degré de contradiction dans les bases de connaissances :

Mesure Contension = 3.0 : - Nombre minimal de variables a assigner pour trouver un modèle partiel - La KB contient des contradictions sur a, b, c, d -> au moins 3 variables problematiques - Interpretation : “Il faut ignorer 3 variables pour rendre la KB coherente”

Mesures basees sur la distance de Dalal :

Mesure Valeur Interpretation
DSum 3.0 Somme des distances aux mondes les plus proches
DMax 2.0 Distance maximale (pire cas)
DHit 1.0 Nombre de mondes a distance minimale

Pour {a && b && c, !a && !b && !c} : - Les deux formules sont completement opposees (distance 3 bits) - DMax = 2 car le monde le plus proche doit flipper 2 variables - DHit = 1 car un seul monde realise cette distance minimale

Mesures Ma et Mcsc (basees sur MUS) : - Ma = 2.0 : Nombre de MUS (Minimal Unsatisfiable Subsets) - Mcsc = 4.0 : Taille du plus grand MCS (Maximal Consistent Subset)

Ces mesures sont utiles pour : - Comparer la gravite de l’incoherence entre bases - Guider la reparation (retirer les formules les plus impliquees dans les MUS)

3.3 Énumération de MUS (Minimal Unsatisfiable Subsets)

Un Sous-ensemble Minimal Inconsistant (MUS) d’une base de connaissances \(KB\) est un sous-ensemble \(M \subseteq KB\) tel que \(M\) est inconsistant, mais tout sous-ensemble propre de \(M\) est consistant. Trouver les MUS est utile pour diagnostiquer les sources d’incohérence.

  • NaiveMusEnumerator: Implémentation simple mais potentiellement très lente, intégrée à Tweety.
  • MarcoMusEnumerator: Interface avec l’outil externe marco.py, beaucoup plus efficace. Nécessite d’installer MARCO et de fournir le chemin vers marco.py.

Applications pratiques des MUS

Les MUS (Minimal Unsatisfiable Subsets) ont des applications concrètes en ingénierie logicielle et IA :

Déboggage de spécifications : - Identifier les exigences contradictoires dans un cahier des charges - Exemple : {HTTPS_requis, Pas_de_chiffrement, Performance_max} → MUS = {HTTPS_requis, Pas_de_chiffrement}

Diagnostic de pannes : - Trouver les combinaisons minimales de défaillances expliquant une panne - Exemple : Système de vol {Capteur_A_OK, Capteur_B_KO, Redondance_active, Alarme_OFF} → MUS indique les causes racines

Réparation automatique : - Supprimer une formule de chaque MUS pour restaurer la cohérence - Minimise le nombre de modifications

Différence Naive vs MARCO : - NaiveMusEnumerator : Algorithme exhaustif, \(O(2^n)\) dans le pire cas - MARCO : Algorithme de map-solving avec Z3, exploite les symétries, peut gérer des centaines de clauses

Le code ci-dessous compare les deux approches.

# --- 3.3 Enumeration de MUS ---
# MUS = Minimal Unsatisfiable Subsets
# Utile pour diagnostiquer les sources d'incoherence dans une base de connaissances

print("\n--- 3.3 Enumeration de MUS (Minimal Unsatisfiable Subsets) ---")

if not jvm_ready:
    print("ERREUR: JVM non demarree.")
else:
    print("JVM prete. Execution de l'exemple MUS...")
    try:
        from org.tweetyproject.logics.pl.parser import PlParser
        from org.tweetyproject.logics.pl.syntax import PlBeliefSet
        from org.tweetyproject.logics.pl.sat import Sat4jSolver, SatSolver
        from org.tweetyproject.logics.commons.analysis import NaiveMusEnumerator
        import subprocess
        import sys
        import tempfile
        import pathlib

        # --- Configuration ---
        parser_mus = PlParser()
        SatSolver.setDefaultSolver(Sat4jSolver())

        # Exemple simple (MusExample.java simplifie)
        kb_mus_ex = PlBeliefSet()
        formulas_mus_ex = ["a", "!a", "!a && !b", "b", "c", "!c", "!a || !c"]
        for f_str in formulas_mus_ex: kb_mus_ex.add(parser_mus.parseFormula(f_str))

        print("KB pour MUS:")
        for f in kb_mus_ex:
            print(f"  - {f}")

        # --- Enumeration ---

        # Option 1: NaiveMusEnumerator (integre a Tweety)
        print("\nCalcul des MUS (Naive Enumerator - peut etre lent sur grandes KB):")
        try:
            mus_enum_naive = NaiveMusEnumerator(SatSolver.getDefaultSolver())
            all_mus_naive = mus_enum_naive.minimalInconsistentSubsets(kb_mus_ex)
            print(f" - Trouve {len(all_mus_naive)} MUS:")
            for mus in all_mus_naive:
                mus_str = ", ".join([str(f) for f in mus])
                print(f"   - {{ {mus_str} }}")
        except Exception as e:
            print(f"Erreur NaiveMusEnumerator: {e}")

        # Option 2: MARCO MUS Enumerator (Python script avec Z3)
        print("\n--- MARCO MUS Enumerator (Script Python + Z3) ---")
        
        # Auto-detection du script marco.py
        marco_paths = [
            pathlib.Path("../ext_tools/marco.py"),
            pathlib.Path("ext_tools/marco.py"),
            pathlib.Path("../../ext_tools/marco.py"),
        ]
        
        marco_script = None
        for mp in marco_paths:
            if mp.exists():
                marco_script = mp.resolve()
                break
        
        if marco_script:
            print(f"  MARCO script trouve: {marco_script}")
            
            # Verifier Z3
            try:
                import z3
                z3_version = z3.get_version_string()
                print(f"  Z3 disponible (version {z3_version})")
                
                # Convertir KB en format DIMACS CNF
                # Note: Simplification pour cet exemple - utilise les formules PL existantes
                # En production, il faudrait convertir kb_mus_ex en DIMACS proper
                
                # Creer un fichier temporaire CNF
                with tempfile.NamedTemporaryFile(mode='w', suffix='.cnf', delete=False) as cnf_file:
                    cnf_path = pathlib.Path(cnf_file.name)
                    
                    # Ecrire header DIMACS (simplifie)
                    cnf_file.write("c MUS test from Tweety\n")
                    cnf_file.write("p cnf 7 7\n")  # 7 variables (a,b,c,d,f,g + negs), 7 clauses
                    
                    # Convertir formules en clauses DIMACS (mapping simple)
                    # a=1, b=2, c=3, d=4, f=5, g=6
                    # Clauses:
                    cnf_file.write("1 0\n")        # a
                    cnf_file.write("-1 0\n")       # !a
                    cnf_file.write("-1 -2 0\n")    # !a && !b -> -1 0, -2 0 (deux clauses) - simplifie en disjonction
                    cnf_file.write("2 0\n")        # b
                    cnf_file.write("3 0\n")        # c
                    cnf_file.write("-3 0\n")       # !c
                    cnf_file.write("-1 -3 0\n")    # !a || !c
                
                try:
                    # Executer marco.py avec --mus-only
                    result = subprocess.run(
                        [sys.executable, str(marco_script), str(cnf_path), "--mus-only"],
                        capture_output=True,
                        text=True,
                        encoding="utf-8",
                        errors="replace",
                        timeout=10
                    )
                    
                    if result.returncode == 0:
                        print("  Resultats MARCO:")
                        for line in result.stdout.strip().split('\n'):
                            if line.startswith("U"):
                                print(f"    MUS: {line}")
                    else:
                        print(f"  Erreur execution MARCO: {result.stderr}")
                    
                except subprocess.TimeoutExpired:
                    print("  Timeout execution MARCO (>10s)")
                except Exception as e_marco:
                    print(f"  Erreur subprocess MARCO: {e_marco}")
                finally:
                    # Cleanup fichier temporaire
                    cnf_path.unlink(missing_ok=True)
                    
            except ImportError:
                print("  Z3 non disponible - installez avec: pip install z3-solver")
        else:
            print("  MARCO script non trouve dans ext_tools/")
            print("  L'outil est disponible dans le depot - verifiez le chemin.")

    except ImportError as e:
        print(f"Erreur d'import pour MUS: {e}")
    except jpype.JException as e_java:
        print(f"Erreur Java dans MUS: {e_java.message()}")
    except Exception as e_gen:
        print(f"Erreur Python inattendue dans MUS: {e_gen}")
        import traceback; traceback.print_exc()

--- 3.3 Enumeration de MUS (Minimal Unsatisfiable Subsets) ---
JVM prete. Execution de l'exemple MUS...
KB pour MUS:
  - !a&&!b
  - !a||!c
  - !a
  - a
  - b
  - !c
  - c

Calcul des MUS (Naive Enumerator - peut etre lent sur grandes KB):
 - Trouve 5 MUS:
   - { !c, c }
   - { !a||!c, a, c }
   - { !a&&!b, a }
   - { !a&&!b, b }
   - { !a, a }

--- MARCO MUS Enumerator (Script Python + Z3) ---
  MARCO script trouve: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\marco.py
  Z3 disponible (version 4.15.3)
  Resultats MARCO:
    MUS: U 0 1
    MUS: U 0 2 3
    MUS: U 4 5
    MUS: U 0 4 6

Interprétation des résultats MUS

Résultats NaiveMusEnumerator : 5 MUS trouvés

MUS Formules Interprétation
1 {!c, c} Conflit direct sur c
2 {!a\|\|!c, a, c} Clause !a\|\|!c incompatible avec a et c simultanément
3 {!a&&!b, a} Conjonction !a&&!b implique !a, contredit a
4 {!a&&!b, b} Conjonction !a&&!b implique !b, contredit b
5 {!a, a} Conflit direct sur a

Résultats MARCO : 4 MUS encodés en DIMACS

  • U 0 1 : Clauses 0 et 1 (mapping : a et !a)
  • U 0 2 3 : Clauses 0, 2, 3 (mapping : a, puis deux autres)
  • U 4 5 : Clauses 4 et 5 (mapping : c et !c)
  • U 0 4 6 : Clauses 0, 4, 6 (mapping : impliquant a, c, et clause 6)

Note : Les indices DIMACS commencent à 0 dans la sortie MARCO. La différence entre les résultats Naive (5 MUS) et MARCO (4 MUS) vient de l’encodage CNF simplifié - en production, il faut convertir correctement les formules PL en DIMACS.

Stratégie de réparation : Supprimer au moins une formule par MUS. Ici, retirer {a, b, c} résoudrait tous les conflits (mais trop agressif). Une approche incrémentale consisterait à retirer !a&&!b qui apparaît dans 2 MUS.

# --- Exercice : Enumeration de MUS pour une politique de securite reseau ---
# TODO etudiant : identifier les MUS d'une politique de pare-feu contradictoire.
# Etape 1 : Construire la KB avec les 6 formules de regles reseau
# Etape 2 : Verifier l'inconsistance avec Sat4jSolver
# Etape 3 : Enumerer les MUS (NaiveMusEnumerator ou methode manuelle)
# Etape 4 : Calculer le hitting set minimal pour la reparation

print("Exercice a completer")
Exercice a completer

Exercice : Enumeration de MUS pour une politique de securite reseau

Un administrateur reseau configure un pare-feu avec les règles suivantes : 1. ssh => !http (SSH bloquant HTTP) 2. ssh => https (SSH active HTTPS) 3. http => https (HTTP implique HTTPS) 4. ssh (SSH est actif) 5. !https (HTTPS est bloque par politique) 6. http (HTTP est autorise)

Objectifs : 1. Construisez la base de connaissances avec ces 6 formules 2. Verifiez que la KB est inconsistante 3. Enumerez les MUS avec NaiveMusEnumerator ou l’approche manuelle (itertools.combinations) 4. Identifiez la reparation minimale (hitting set des MUS)

Indices : - Reutilisez le pattern de l’exemple guide meteo : PlParser, PlBeliefSet, Sat4jSolver - NaiveMusEnumerator(SatSolver.getDefaultSolver()).minimalInconsistentSubsets(kb) pour l’enumeration directe - Cherchez le plus petit ensemble de formules a retirer qui intersecte chaque MUS

3.4 MaxSAT

MaxSAT (Maximum Satisfiability) est une généralisation du problème SAT. Étant donné un ensemble de clauses “dures” (qui doivent être satisfaites) et un ensemble de clauses “molles” (qui peuvent être violées, souvent avec un coût/poids associé), MaxSAT cherche une assignation qui satisfait toutes les clauses dures et minimise le coût total des clauses molles violées (ou maximise le poids des clauses molles satisfaites).

Tweety intègre des solveurs MaxSAT externes comme Open-WBO.

  • MaxSatSolver: Interface abstraite.
  • OpenWboSolver: Implémentation pour Open-WBO (nécessite chemin).
  • Entrée: Une PlBeliefSet pour les clauses dures, et une Map<PlFormula, Integer> pour les clauses molles et leurs poids (coûts de violation).
  • Sortie: Une Interpretation (un PossibleWorld) qui est une solution optimale.
# --- 3.4.1 MaxSAT : Configuration et Imports ---
print("--- 3.4.1 MaxSAT : Configuration ---")

if not jvm_ready:
    print("ERREUR: JVM non demarree.")
    maxsat_imports_ok = False
else:
    maxsat_imports_ok = False
    try:
        from org.tweetyproject.logics.pl.parser import PlParser
        from org.tweetyproject.logics.pl.syntax import PlBeliefSet
        from java.util import HashMap
        import subprocess
        import tempfile
        import pathlib
        
        parser_maxsat = PlParser()
        print("Imports MaxSAT reussis.")
        maxsat_imports_ok = True
        
    except ImportError as e:
        print(f"ERREUR d'import : {e}")
--- 3.4.1 MaxSAT : Configuration ---
Imports MaxSAT reussis.

Transition : De MUS à MaxSAT

MUS identifie les conflits minimaux, mais ne résout pas le problème de satisfaction partielle optimale. Scénario :

Problème : Une base de connaissances avec : - Contraintes dures : Règles métier obligatoires (ex: !fraude, transaction_valide) - Préférences molles : Souhaits de l’utilisateur avec coûts de violation (ex: livraison_rapide poids 10, prix_bas poids 5)

Question : Quelle assignation satisfait toutes les contraintes dures et minimise les violations pondérées des préférences ?

Réponse : MaxSAT (Maximum Satisfiability)

Type de clause Traitement Exemple
Dure Doit être satisfaite Lois, règles de sécurité
Molle Peut être violée avec coût Préférences utilisateur, optimisations

Les solveurs MaxSAT (comme RC2 de pySAT) trouvent l’assignation optimale en temps polynomial pour la plupart des instances pratiques.

Definition des clauses MaxSAT

MaxSAT distingue deux types de clauses : - Clauses dures : doivent etre satisfaites (contraintes obligatoires) - Clauses molles : ont un poids/cout de violation (optimisation)

# --- 3.4.2 Definition des clauses MaxSAT ---
if maxsat_imports_ok:
    # Clauses Dures (doivent etre satisfaites)
    hard_clauses_bs = PlBeliefSet()
    hard_formulas = ["!a && b", "b || c", "c || d", "f || (c && g)"]
    for f_str in hard_formulas:
        hard_clauses_bs.add(parser_maxsat.parseFormula(f_str))
    
    # Clauses Molles (avec poids de violation)
    soft_clauses_map = HashMap()
    soft_clauses_map.put(parser_maxsat.parseFormula("a || !b"), 25)  # violer coute 25
    soft_clauses_map.put(parser_maxsat.parseFormula("!c"), 15)       # violer coute 15
    
    print("Clauses Dures:")
    for f in hard_clauses_bs:
        print(f"  {f}")
    
    print("\nClauses Molles:")
    for entry in soft_clauses_map.entrySet():
        print(f"  {entry.getKey()} (poids: {entry.getValue()})")
else:
    print("Imports MaxSAT non disponibles.")
Clauses Dures:
  b||c
  c||d
  !a&&b
  f||(c&&g)

Clauses Molles:
  a||!b (poids: 25)
  !c (poids: 15)

Resolution MaxSAT avec RC2

RC2 (Relaxable Cardinality Constraints) est le solveur MaxSAT de pySAT, vainqueur de MaxSAT Evaluation 2018.

Le format WCNF (Weighted CNF) encode les clauses avec poids :

p wcnf <nb_vars> <nb_clauses> <top_weight>
<weight> <lit1> <lit2> ... 0
# --- 3.4.3 Resolution MaxSAT avec RC2 ---
if maxsat_imports_ok:
    # Detecter le script maxsat_solver.py
    maxsat_paths = [
        pathlib.Path("../ext_tools/maxsat_solver.py"),
        pathlib.Path("ext_tools/maxsat_solver.py"),
    ]
    
    maxsat_script = None
    for mp in maxsat_paths:
        if mp.exists():
            maxsat_script = mp.resolve()
            break
    
    if maxsat_script:
        print(f"MaxSAT script: {maxsat_script}")
        
        try:
            import sys
            import pysat
            print(f"PySAT version: {pysat.__version__}")
            
            # Creer fichier WCNF temporaire
            with tempfile.NamedTemporaryFile(mode='w', suffix='.wcnf', delete=False) as wcnf_file:
                wcnf_path = pathlib.Path(wcnf_file.name)
                top_weight = 1000
                
                wcnf_file.write(f"p wcnf 6 7 {top_weight}\n")
                # Clauses dures
                wcnf_file.write(f"{top_weight} -1 0\n")      # !a
                wcnf_file.write(f"{top_weight} 2 0\n")       # b
                wcnf_file.write(f"{top_weight} 2 3 0\n")     # b || c
                wcnf_file.write(f"{top_weight} 3 4 0\n")     # c || d
                wcnf_file.write(f"{top_weight} 5 3 6 0\n")   # f || c || g
                # Clauses molles
                wcnf_file.write("25 1 -2 0\n")              # a || !b, poids 25
                wcnf_file.write("15 -3 0\n")                # !c, poids 15
            
            # Executer le solveur
            result = subprocess.run(
                [sys.executable, str(maxsat_script), str(wcnf_path)],
                capture_output=True, text=True, encoding="utf-8", errors="replace", timeout=10
            )
            
            if result.returncode == 0:
                print("\nResultats MaxSAT:")
                var_map = {1: 'a', 2: 'b', 3: 'c', 4: 'd', 5: 'f', 6: 'g'}
                for line in result.stdout.strip().split('\n'):
                    if line.startswith("s "):
                        print(f"  Status: {line[2:]}")
                    elif line.startswith("o "):
                        print(f"  Cout optimal: {line[2:]}")
                    elif line.startswith("v "):
                        lits = [int(x) for x in line[2:].split() if x != '0']
                        assignment = [f"{var_map[abs(l)]}={l>0}" for l in lits if abs(l) in var_map]
                        print(f"  Assignation: {', '.join(assignment)}")
            else:
                if "pysat.examples" in result.stderr or "No module named 'pysat'" in result.stderr:
                    print("ATTENTION: python-sat (pysat.examples.rc2) introuvable dans ce kernel.")
                    print("Cause: package satellite-science 'pysat' qui masque 'python-sat',")
                    print("ou kernel actif != 'epita_symbolic_ai'. Selectionnez le kernel 'epita_symbolic_ai'.")
                else:
                    print(f"Erreur: {result.stderr}")
            
            wcnf_path.unlink(missing_ok=True)
            
        except ImportError:
            print("PySAT non disponible")
    else:
        print("Script maxsat_solver.py non trouve")
else:
    print("Imports MaxSAT non disponibles.")
MaxSAT script: <repo>MyIA.AI.Notebooks\SymbolicAI\ext_tools\maxsat_solver.py
PySAT version: 1.9.dev4

Resultats MaxSAT:
  Status: OPTIMUM FOUND
  Cout optimal: 25
  Assignation: a=False, b=True, c=False, d=True, f=True, g=False

Interprétation des résultats MaxSAT

Problème MaxSAT posé :

Clauses dures (poids 1000, doivent être satisfaites) : - !a (négation de a) - b (obligation) - b || c (au moins un des deux) - c || d (au moins un des deux) - f || c || g (au moins un des trois)

Clauses molles (peuvent être violées) : - a || !b (poids 25) : Préférence pour a vrai ou b faux - !c (poids 15) : Préférence pour c faux

Solution optimale trouvée par RC2 :

a=False, b=True, c=False, d=True, f=True, g=False

Analyse :

Variable Valeur Justification
a False Imposé par clause dure !a
b True Imposé par clause dure b
c False Préférence molle !c (poids 15) respectée
d True Nécessaire car c=False et clause dure c \|\| d
f True Nécessaire car c=False, g=False et clause dure f \|\| c \|\| g
g False Choix libre, minimise les variables vraies

Coût total : 25 (seule la clause molle a || !b est violée, car a=False et b=True)

Vérification : - a || !b : False || False = False → violée, coût 25 - !c : True → satisfaite, coût 0

Note : RC2 a trouvé l’optimum global. La clause molle a || !b est structurellement toujours violée : les contraintes dures !a (donc a=False) et b (donc b=True) la rendent fausse dans tous les cas, si bien que son coût de 25 est inévitable. Le seul vrai degré de liberté est la clause !c : forcer c=True la violerait (coût 15) en plus du 25 inévitable, soit un total de 40 — supérieur à l’optimum. En respectant !c (c=False, comme RC2 l’a fait), le coût reste 25, qui est bien le minimum atteignable.

# --- Exercice : Formulation MaxSAT pour un planning de ressources ---
# TODO etudiant : formuler et resoudre un probleme MaxSAT de planification.
# Etape 1 : Definir les variables (alice=a, bob=b, charlie=c, delta=d)
# Etape 2 : Definir les clauses dures et molles avec leurs poids
# Etape 3 : Enumerer les assignations valides (respectant les clauses dures)
# Etape 4 : Trouver l'assignation qui minimise le cout des clauses molles violees

print("Exercice a completer")
Exercice a completer

Exercice : Formulation MaxSAT pour un planning de ressources

Un chef de projet doit planifier les ressources d’une équipe avec les contraintes suivantes :

Contraintes dures (doivent etre respectees) : 1. alice || bob (au moins un membre de l’équipe principale est assigne) 2. alice => !bob (Alice et Bob ne peuvent pas travailler ensemble sur ce projet) 3. charlie || delta (au moins un membre de l’équipe secondaire est assigne) 4. delta => alice (si Delta travaille, Alice doit aussi travailler)

Préférences molles (peuvent etre violees avec un cout) : 5. !alice (Alice est couteuse, poids 20) 6. charlie (Charlie est disponible, poids 10) 7. !delta (Delta est junior, poids 5)

Objectifs : 1. Definissez les clauses dures et molles avec leurs poids 2. Formulez le problème en format WCNF 3. Trouvez manuellement l’assignation optimale (ou utilisez un solveur si disponible) 4. Calculez le cout total et verifiez que toutes les clauses dures sont satisfaites

Indices : - Representez les variables : alice=a, bob=b, charlie=c, delta=d - En format WCNF, les clauses dures ont le poids top_weight (ex: 1000) - Enumerez les combinaisons possibles et eliminez celles qui violent les clauses dures - Parmi les combinaisons valides, choisissez celle qui minimise le cout des clauses molles violees

Exemple guide : Diagnostic d’incoherence dans une base de règles meteo

Contexte

Une station meteo automatisee produit les règles suivantes (certaines contradictoires) : 1. soleil => sec (s’il fait soleil, il fait sec) 2. pluie => !sec (s’il pleut, il ne fait pas sec) 3. soleil (il fait soleil) 4. pluie (il pleut) 5. vent => froid (s’il y a du vent, il fait froid) 6. soleil => !froid (s’il fait soleil, il ne fait pas froid) 7. vent (il y a du vent)

Objectifs

  1. Construire la KB avec les 7 formules en logique propositionnelle
  2. Verifier que la KB est inconsistante
  3. Calculer une mesure d’incoherence (par exemple, le nombre de MUS)
  4. Identifier les sous-ensembles minimaux inconsistants (MUS)
  5. Proposer la reparation minimale (quelles formules retirer pour restaurer la coherence ?)

Indices :

  • Utilisez PlParser pour parser les formules et PlBeliefSet pour la KB
  • SatReasoner().isConsistent(kb) pour verifier la consistance
  • Pour les MUS, utilisez PlMusEnumerator ou une approche manuelle (retirer une formule a la fois)
  • La KB contient 2 conflits independants : {1,2,3,4} et {1,5,6,3,7} - trouvez les MUS exacts
# --- Exemple guide : Diagnostic d'incoherence meteo ---
# Solution complete : identification des MUS et reparation minimale d'une base de regles meteo.

if jvm_ready:
    import itertools

    from org.tweetyproject.logics.pl.syntax import PlBeliefSet
    from org.tweetyproject.logics.pl.parser import PlParser
    from org.tweetyproject.logics.pl.sat import Sat4jSolver, SatSolver

    SatSolver.setDefaultSolver(Sat4jSolver())
    solver = SatSolver.getDefaultSolver()
    parser = PlParser()

    # 1. Les 7 formules du probleme (donnees de l'exercice)
    formulas_str = [
        "soleil => sec",
        "pluie => !sec",
        "soleil",
        "pluie",
        "vent => froid",
        "soleil => !froid",
        "vent",
    ]

    # 2. Construire la KB
    formulas = [parser.parseFormula(f) for f in formulas_str]
    kb = PlBeliefSet()
    for f in formulas:
        kb.add(f)
    print(f"KB construite avec {len(formulas)} formules.")

    # 3. Verifier l'inconsistance
    kb_consistante = solver.isConsistent(kb)
    print("KB consistante ?", kb_consistante)

    # 4. Trouver les MUS (approche manuelle)
    # Pour chaque sous-ensemble de formules, verifier s'il est inconsistant
    # et s'il est minimal (retirer une formule le rend consistant)
    # Indice: utilisez itertools.combinations
    indices = list(range(len(formulas)))

    def sub_kb(idx_set):
        bs = PlBeliefSet()
        for i in idx_set:
            bs.add(formulas[i])
        return bs

    def est_incoherent(idx_set):
        return not solver.isConsistent(sub_kb(idx_set))

    mus_list = []
    for taille in range(1, len(formulas) + 1):
        for combo in itertools.combinations(indices, taille):
            s = set(combo)
            # Sur-ensemble d'un MUS deja trouve => non minimal, on saute
            if any(m.issubset(s) for m in mus_list):
                continue
            if est_incoherent(s):
                # Minimalite : retirer une formule rend la KB consistante
                minimal = all(not est_incoherent(s - {i}) for i in s)
                if minimal:
                    mus_list.append(s)

    print(f"\nNombre de MUS trouves : {len(mus_list)}")
    for k, mus in enumerate(mus_list, 1):
        contenu = [formulas_str[i] for i in sorted(mus)]
        print(f"  MUS {k} (taille {len(mus)}) : {contenu}")

    # 5. Proposer la reparation minimale
    # Quelles formules retirer pour restaurer la coherence ?
    # (Chercher un "hitting set" minimal des MUS)
    hitting_set = None
    for taille in range(1, len(formulas) + 1):
        for combo in itertools.combinations(indices, taille):
            h = set(combo)
            if all(h & mus for mus in mus_list):
                hitting_set = h
                break
        if hitting_set is not None:
            break

    a_retirer = [formulas_str[i] for i in sorted(hitting_set)]
    print(f"\nReparation minimale : retirer {len(hitting_set)} formule(s) -> {a_retirer}")

    restantes = set(indices) - hitting_set
    kb_reparee = sub_kb(restantes)
    print(f"KB reparee consistante ? {solver.isConsistent(kb_reparee)}")
else:
    print("Skipped: JVM non demarree.")
KB construite avec 7 formules.
KB consistante ? False

Nombre de MUS trouves : 2
  MUS 1 (taille 4) : ['soleil => sec', 'pluie => !sec', 'soleil', 'pluie']
  MUS 2 (taille 4) : ['soleil', 'vent => froid', 'soleil => !froid', 'vent']

Reparation minimale : retirer 1 formule(s) -> ['soleil']
KB reparee consistante ? True

Resume et perspectives

Ce notebook a couvert les mécanismes de revision de croyances et d’analyse d’incoherence dans les bases de connaissances propositionnelles. La revision multi-agents (CrMas) a montre comment trois opérateurs – Levi, Simple et Argumentatif – gerent differemment les conflits entre sources d’information ordonnees par credibilite. Les mesures d’incoherence (Contension, DSum, DMax, DHit, Ma, Mcsc) fournissent des metriques quantitatives pour evaluer la gravite des contradictions. L’enumeration des MUS (Minimal Unsatisfiable Subsets) via l’algorithme NaiveMusEnumerator identifie les sous-ensembles minimaux de formules responsables de l’inconsistance, tandis que MaxSAT avec le solveur RC2 optimise la satisfaction des contraintes en distinguant clauses dures et molles.

L’exemple guide sur le diagnostic meteorologique a illustre le workflow complet de diagnostic d’incoherence : construction de la base de connaissances, verification d’inconsistance, identification des MUS par enumeration exhaustive, et reparation minimale par hitting set. Ce processus est transposable a de nombreux domaines reels : diagnostic medical (règles contradictoires entre symptomes), verification de logiciels (exigences incompatibles), et integration de données multi-sources (capteurs IoT, reseaux sociaux). La cle reside dans l’identification des conflits minimaux (MUS) qui permettent une reparation ciblee plutot qu’un remplacement massif des connaissances. Les limitations rencontrees avec l’API CrMas (refactorisation dans Tweety 1.28+) et la dépendance aux solveurs externes (MARCO pour les grandes instances) soulignent l’importance de l’ecosysteme d’outils dans l’applicabilite de ces méthodes.

Le notebook suivant, Tweety-5-Abstract-Argumentation, explore l’argumentation abstraite et les frameworks de Dung, ou les conflits entre arguments sont resolus par des relations d’attaque plutot que par des mesures numériques d’incoherence.

Resume

Ce notebook a couvert :

Section Concepts cles
3.1 CrMas Revision de croyances multi-agents, ordre de credibilite, AGM
3.2 Mesures Mesures d’incoherence (contension, drastic, MI, MIC)
3.3 MUS Sous-ensembles minimaux insatisfiables, diagnostic
3.4 MaxSAT Clauses dures/molles, optimisation, RC2 solver

Points cles: - La revision de croyances gere les conflits entre informations - Les mesures d’incoherence quantifient les contradictions - MUS identifie les sources minimales de conflits - MaxSAT optimise la satisfaction des contraintes avec préférences

Prochaines étapes

Le notebook suivant explore l’argumentation abstraite (frameworks de Dung).

Navigation: Tweety-3-Advanced-Logics | Index | Tweety-5-Abstract-Argumentation

Exercice : Diagnostic d’incoherence dans un système de diagnostic medical

Un système expert medical contient les règles suivantes : 1. fievre => infection (la fievre indique une infection) 2. infection => antibiotic (une infection necessite des antibiotiques) 3. virus => !antibiotic (un virus ne necessite pas d’antibiotiques) 4. fievre (le patient a de la fievre) 5. virus (le patient a un virus) 6. virus => infection (un virus est une infection)

Questions : 1. La KB est-elle consistante ? 2. Identifiez les MUS 3. Proposez une reparation minimale

Indices : - Reutilisez le pattern de l’exemple guide : PlParser, PlBeliefSet, Sat4jSolver - Enumerez les sous-ensembles avec itertools.combinations - Cherchez un hitting set minimal des MUS

# --- Exercice : Diagnostic d'incoherence dans un systeme de diagnostic medical ---
# TODO etudiant : identifier les MUS d'une base de regles medicale.
# Etape 1 : Construire la KB avec les formules donnees
# Etape 2 : Verifier l'inconsistance
# Etape 3 : Identifier les MUS (methode manuelle ou NaiveMusEnumerator)
# Etape 4 : Proposer une reparation minimale

print("Exercice a completer")
Exercice a completer
Retour au sommet