Argumentation strate 6 — Acceptabilité QBF : quantificateurs par énumération, crédule et sceptique
Série : ICT-Series (strate 6, argumentation) · Epic#4588 · Grain#17339 — distillation Triple Distillation (mandat user 2026-09-21), volet ICT.
Ce carnet est le troisième de la famille ICT-Argumentation-* : après les trajectoires de croyance Dung (ICT-Argumentation-BeliefTrajectories) et la mémoire de justification JTMS/ATMS (ICT-Argumentation-TruthMaintenance, PR #17324), il ajoute l’angle complexité computationnelle : lire l’acceptabilité d’un argument comme une formule booléenne quantifiée (QBF) — et la résoudre à la main, par énumération naïve, pour voir ce que « quantifier » veut dire.
Cadre. Une QBF est une formule propositionnelle dont les variables sont préfixées de quantificateurs ∀ (pour tout) et ∃ (il existe). Décider si une QBF est valide est le problème canonique PSPACE-complet (Papadimitriou 1994) : chaque bloc de quantificateurs multiplie le travail de l’évaluateur. Notre moteur n’est PAS un solveur SOTA — c’est le contraire assumé : une énumération exhaustive en 2^n qui rend chaque quantificateur visible comme une boucle. C’est précisément la leçon : le quantificateur n’est pas une notation, c’est un coût.
Statut épistémique. Ce carnat est une restitution pédagogique mesurée : les sorties committées proviennent d’un port dont la fidélité à la source est prouvée par exécution différentielle (16/16 surfaces identiques, tête a5ac1a5d) et par des littéraux figés dans ict/tests/test_qbf.py (21 gates). Aucun chiffre de ce carnet n’est écrit à la main : chaque valeur citée dans la prose est lue sur la sortie committée de la cellule qui la produit.
Organ-first — copie pédagogique déclarée. Le moteur ict/qbf.py est un port déclaré du module EPITA argumentation_analysis/agents/core/logic/qbf_native.py (né au commit 0d2ac1b0, PR EPITA #167), enseigné par le notebook EPITA belief_revision.ipynb §5. Aucun moteur QBF n’existe sous forme d’organe invoquable dans ce dépôt : la seule sémantique Dung réelle vit dans ict/argumentation.py, que ce grain étend d’une fonction preferred_extensions (l’organe calcule désormais la sémantique dont la question sceptique a besoin). Les détails vivent dans la section conclusion.
1. Setup — les organes
Deux organes : ict.argumentation (cadres de Dung, labeling grounded — et depuis ce grain, extensions préférées) et ict.qbf (AST à quantificateurs, parseur, énumérateur, acceptabilité crédule/sceptique). Convention de la série : numpy-free, déterminisme complet, CPU pur. Les sorties n’impriment que des basename — aucun chemin machine.
2. Quantificateurs : ce que « pour tout » et « il existe » coûtent
2.1 Les deux cas extrêmes
La tautologie et la contradiction sont les bornes : la première valide quelle que soit la valeur de x, la seconde invalide quelle que soit la recherche d’un témoin. Remarquez le vocabulaire du verdict : VALID / INVALID — le moteur parle le langage des QBF, pas celui des ensembles de modèles.
(True, 'QBF VALID: x | !x')
(False, 'QBF INVALID: x & !x')
2.2 L’alternance — et pourquoi l’ordre n’est pas commutatif
Le cœur du sujet n’est pas chaque quantificateur isolé mais leur alternance. Prenons la matrice d’équivalence x & y | !x & !y (lue : x == y). Les deux préfixes possibles à deux blocs rendent des verdicts opposés sur la même matrice :
exists x. forall y. (x == y) — invalide : on choisit x d’abord, puis l’adversaire (forall) choisit y pour démentir. Un seul choix ne peut pas couvrir deux valeurs.
forall y. exists x. (x == y) — valide : l’adversaire bouge d’abord, et le répondant copie. Répondre après est plus fort que jouer avant.
Cette lecture stratégique (le joueur existentiel contre le joueur universel) est exactement la sémantique des jeux des QBF : chaque préfixe est un ord de jeu. L’énumération naïve la matérialise — boucle imbriquée après boucle imbriquée.
exists x. forall y . (x == y) -> False
forall y. exists x . (x == y) -> True
2.3 Trois blocs : le répondant intérieur
À trois blocs, la même logique se poursuit un cran plus loin. Sur la matrice à trois clauses a & b | !b & c | !a & !c, le préfixe exists a. forall b. exists c. est valide : le premier joueur pose a = Vrai, l’adversaire choisit b, et le répondant intérieur crépond à b (c = Vrai si b = Faux). Le quantificateur le plus interne joue en dernier — c’est lui qui dispose de l’information de tous les coups précédents.
True - QBF VALID: a & b | !b & c | !a & !c
search_space = 8 | variables = 3 | blocs = 2
La statistique search_space = 8 est le prix affiché : trois variables, 2**3 = 8 feuilles au pire cas. C’est là que la leçon de complexité se tient : ajouter une variable double l’espace ; ajouter un bloc quantifié en déplace la structure. Un solveur SOTA (résolution, expansion de préfixe) fait mieux que l’énumération — mais l’énumération est la seule méthode qui montre le problème en entier, feuille par feuille, raison pour laquelle ce moteur pédagogique l’assume et la déclare.
Cette grille de lecture stratégique se réutilise telle quelle en théorie des jeux : un préfixe QBF est un jeu à information parfaite où les joueurs posent leurs variables à tour de rôle, le joueur ∃ cherchant à rendre la matrice vraie, le joueur ∀ à la rendre fausse. La QBF est valide exactement quand le joueur ∃ a une stratégie gagnante — une fonction qui, à chaque coup adverse, associe une réponse correcte. C’est pourquoi l’ordre compte : une stratégie doit répondre au coup précédent, pas le deviner. Le répondant intérieur d’une alternance ∃∀∃ voit les coups de ses deux adversaires successifs ; le quantificateur externe, lui, joue à l’aveugle. Toute la hiérarchie polynomiale (∃, ∀, ∃∀, ∀∃…) se relit ainsi : une échelle d’information décroissante pour le joueur existentiel.
3. Le parseur : précédences, et une limite assumée
La formule arrive en chaîne ("x => y"), pas en AST. Le parseur applique les précédences ! > & > | > => — l’implication est la plus faible. Limite héritée de la source et enseignée ici : pas de parenthèses. Le repr de l’AST montre la structure retenue, et avec elle le piège : a & b | c se lit (a & b) | c, jamais a & (b | c).
f = qbf.parse_formula("a & b | c")print(type(f).__name__, '->', repr(f))g = qbf.parse_formula("a => b & c")print(type(g).__name__, '->', repr(g))# => est la plus faible : a => (b & c), jamais (a => b) & c.assertrepr(g) =='(a => (b & c))'
Or -> ((a & b) | c)
Implies -> (a => (b & c))
Ce choix n’est pas un bug silencieux : il est documenté dans la docstring du module et épingle par un test (test_parseur_precedences_sans_parentheses). En pédagogie, une limite montrée vaut mieux qu’une généralité cachée : l’étudiant voit qu’un parseur sans parenthèses n’est pas neutre — il choisit une lecture pour vous.
4. Acceptabilité crédule : l’énumération EST le quantificateur
Revenons à l’argumentation. La question crédule est : existe-t-il une extension admissible qui contienne l’argument target ? Relisez-la : c’est un ∃ — il existe un ensemble, sans conflit, qui se défend, contenant la cible. La fonction credulous_acceptance_qbf ne convertit pas cette question en QBF pour la déléguer à un solveur : elle matérialise le ∃ en énumérant les sous-ensembles (2**n masques binaires croissants) et en s’arrêtant au premier témoin. La recherche de témoin et le quantificateur existentiel sont le même objet vu par la théorie et par le code.
Sur le Nixon diamond à trois arguments (a et b s’attaquent, c est libre), chaque argument est crédulement accepté — mais les témoins racontent des choses différentes :
ARGS = ["a", "b", "c"]ATTACKS = [["a", "b"], ["b", "a"]]for tgt in ARGS: r = qbf.credulous_acceptance_qbf(ARGS, ATTACKS, tgt)print(f"cible {tgt} : accepte={r['accepted']} temoin={r.get('witness_extension')}")# Le temoin est DETERMINISTE : premier masque binaire admissible contenant la cible.assert qbf.credulous_acceptance_qbf(ARGS, ATTACKS, "a")["witness_extension"] == ["a"]
cible a : accepte=True temoin=['a']
cible b : accepte=True temoin=['b']
cible c : accepte=True temoin=['c']
Deux cas limites mesurés, qui distinguent la sémantique d’une intuition vite faite :
La chaîne défensive — d est attaqué par b, lui-même attaqué par a et c. Intuitivement « d est attaqué, donc refusé » ; la mesure dit le contraire : {a, d} est admissible (adéfendd), témoin ['a', 'd']. L’acceptabilité crédule est une question de coalition défensive, pas de statut individuel.
Le cycle impair — a -> b -> c -> a : personne n’est crédulement accepté. Chaque attaquant d’un membre du cycle est un autre membre… qui ne peut pas coexister avec lui (conflit). Le cycle pair (Nixon) laisse deux témoins singleton ; le cycle impair n’en laisse aucun.
# Chaine defensive : le temoin contient DEUX arguments (a defend d).r = qbf.credulous_acceptance_qbf( ["a", "b", "c", "d"], [["a", "b"], ["c", "b"], ["b", "d"]], "d")print('chaine, cible d :', r['accepted'], r['witness_extension'])# Cycle impair : refuse pour TOUTE cible.odd = qbf.credulous_acceptance_qbf( ["a", "b", "c"], [["a", "b"], ["b", "c"], ["c", "a"]], "a")print('cycle impair, cible a :', odd['accepted'], '-', odd['reason'])
chaine, cible d : True ['a', 'd']
cycle impair, cible a : False - No admissible extension contains a
La borne n <= 15 n’est pas une coquetterie : à 16 arguments, 2**16 = 65536 sous-ensembles — l’organe refuse de mesurer (accepted=None, raison explicite) plutôt que de tourner en silence. Un refus visible vaut mieux qu’un temps de calcul caché : c’est la même discipline que le RefusDeMesure du pipeline discursif de la série (arbitrage #7742).
5. Acceptabilité sceptique : le ∀ passe par l’organe natif
La question sceptique inverse le quantificateur : target est-il dans toutes les extensions préférées (maximales pour l’inclusion) ? C’est un ∀ sur les extensions. Ici le port consomme l’organe : la fonction preferred_extensions que ce grain ajoute à ict/argumentation.py énumère les ensembles admissiaux maximaux — le mapping noms→indices vit à la frontière, la sémantique vit dans l’organe.
Sur le Nixon à trois arguments, les extensions préférées sont {a, c} et {b, c} (les singletons {a} et {b} ne sont pas maximaux : c — non attaqué — les complète tous les deux) :
preferred : [['a', 'c'], ['b', 'c']]
a sceptiquement accepte : False - a is NOT in all preferred extensions
c sceptiquement accepte : True
L’exemple Tweety (a et b se contredisent, c attaque b) resserre la lecture : la seule extension préférée est {a, c} — a est cette fois sceptiquement accepté, parce qu’aucne extension préférée ne peut exclure son défenseur structurel. Crédule et sceptique ne sont pas deux forces d’une même question : ce sont deux quantificateurs sur deux collections différentes (∃ sur les admissibles, ∀ sur les préférées).
tweety preferred : [['a', 'c']]
a sceptiquement accepte : True
Récapitulons la dualité telle que le code la montre, colonne par colonne : la question crédule parcourt les admissibles (ensembles sans conflit qui se défendent — sans exigence de maximalité) et s’arrête au premier témoin ; la question sceptique parcourt les préférées (les admissibles maximaux, obtenus par l’organe) et exige la présence dans toutes. Entre les deux collections, la maximalité : elle ne change aucun statut sur les cas symétriques (Nixon), mais elle change tout dès qu’un argument non attaqué vient compléter les mondes possibles — c rejoint chaque préférée du Nixon sans jamais être mis en cause. L’agent crédule et l’agent sceptique divergent exactement là où la structure rend un monde inévitable pour l’un et contingent pour l’autre.
6. Le pont : théorème de Dung relu comme inclusion, et témoin négatif
Il reste à relier les deux organes du grain précédent et celui-ci. Le théorème structurel (Dung 1995) : l’extension grounded est incluse dans chaque extension préférée. Le grounded — construit par point fixe du labeling (voir ICT-Argumentation-BeliefTrajectories) — est le noyau minimal ; chaque préférée est un monde maximal cohérent avec ce noyau. En langage quantifié : ce qui est accepté sans hypothèse (∀ implicite du point fixe) survit dans tous les mondes maximaux.
Le bloc suivant est le témoin négatif du carnet : il échoue si l’organe Dung dérive, si preferred_extensions diverge de la sémantique, ou si le labeling grounded change. Il rejoue l’inclusion sur quatre instances à chaque exécution.
cas = [ ("nixon 2", arg.nixon_diamond()), ("tweety", arg.tweety_bird()), ("chaine a->b", arg.DungAF([0, 1], [(0, 1)])), ("double defense", arg.DungAF([0, 1, 2], [(0, 1), (2, 1), (1, 2)])),]for nom, af in cas: lab = arg.grounded_labeling(af) grounded_in = {a for a, s in lab.items() if s =="in"} prefs = arg.preferred_extensions(af)for ext in prefs:# Theoreme : le noyau grounded survit dans CHAQUE monde maximal.assert grounded_in <= ext, (nom, grounded_in, ext)print(f"{nom:14s} grounded_in={sorted(grounded_in)} "f"preferred={[sorted(e) for e in prefs]}")print("\nTemoin negatif OK : grounded <= chaque preferred sur les 4 instances.")
nixon 2 grounded_in=[] preferred=[[0], [1]]
tweety grounded_in=[0, 2] preferred=[[0, 2]]
chaine a->b grounded_in=[0] preferred=[[0]]
double defense grounded_in=[0, 2] preferred=[[0, 2]]
Temoin negatif OK : grounded <= chaque preferred sur les 4 instances.
Lecture du tableau : le noyau grandit avec la structure défensive (vide pour le Nixon pur — deux undec ; {0, 2} pour Tweety), et chaque préférée le contient. La réciproque est fausse en général — l’intersection des préférées peut strictement dépasser le grounded : c’est précisément l’objet du troisième exercice.
7. Exercices
Trois exercices, stubs conformes C.1 (aucune erreur volontaire : chaque fonction retourne None, le carnet s’exécute de bout en bout même non complété).
def exercice_1_ordre_sensible():"""Construire une matrice a DEUX variables ou l'ordre des quantificateurs decide -- mais dans le sens INVERSE de la section 2.2 : une matrice ou exists x. forall y. est VALIDE et forall y. exists x. est INVALIDE. Etapes : 1. Choisissez une matrice (chaine sans parentheses, operateurs ! & | =>) ou le premier joueur peut figer une valeur qui rend la matrice tautologique, mais ou le repondant ne peut pas suivre. 2. Verifiez les deux ordres avec qbf.check_qbf. 3. Expliquez en une phrase pourquoi le joueur existentiel gagne en jouant en premier ici (et pas sur l'equivalence). Verification attendue : deux appels check_qbf aux verdicts opposes, et une phrase d'explication. """# TODO etudiantreturnNonedef exercice_2_temoin_a_deux():"""Predire le TEMOIN de l'enumeration avant de la lancer. Etapes : 1. Construisez un AF a 4 arguments nommes ou la cible n'est acceptee que dans une extension admissible a deux membres (la cible et son defenseur), comme la chaine defensive de la section 4. 2. Sur papier, listez l'ordre des masques binaires croissants et predisez quel sera le premier temoin trouve. 3. Verifiez avec credulous_acceptance_qbf : le temoin est deterministe (ordre des bits). Verification attendue : witness_extension == ['<defenseur>', '<cible>'] dans l'ordre alphabetique du tri, egal a la prediction. """# TODO etudiantreturnNonedef exercice_3_ecart_grounded_sceptique():"""Construire l'instance ou l'intersection des extensions preferees DEPASSE strictement l'extension grounded (la reciproque fausse du theoreme de la section 6). Etapes : 1. Partez d'un cycle pair (deux undec, grounded vide pour le cycle) et ajoutez un argument NON attaque qui n'attaque rien du cycle : il entre dans le grounded ET dans chaque preferee. 2. Pour decaler strictement, cherchez plutot une structure ou un argument attaque seulement par des undec du cycle est rejoint par un defenseur commun a toutes les preferees. 3. Mesurez : grounded_labeling, preferred_extensions, puis intersection des preferees ; affichez l'ecart strict. Verification attendue : un ensemble non vide d'arguments qui sont dans toutes les preferees mais ni 'in' au sens grounded -- l'ecart sceptique > grounded, affiche par difference d'ensembles. """# TODO etudiantreturnNonefor fn in (exercice_1_ordre_sensible, exercice_2_temoin_a_deux, exercice_3_ecart_grounded_sceptique):print(fn.__name__, '->', fn())
Ce que le carnet a établi. (1) Les quantificateurs booléens se lisent stratégiquement — ordre de jeu, répondant intérieur — et l’ordre n’est pas commutatif (§2). (2) Un parseur à précédences sans parenthèses fait des choix de lecture qu’il faut savoir voir (§3). (3) L’acceptabilité crédule est un ∃ matérialisé par l’énumération des coalitions défensives — la chaîne défensive et le cycle impair sont les deux cas qui cassent l’intuition individuelle (§4). (4) L’acceptabilité sceptique est un ∀ sur les extensions préférées, calculées par l’organe natif Dung que ce grain dote de preferred_extensions (§5). (5) Le théorème grounded ⊆ chaque préférée relie ce grain au carnet Dung précédent — témoin négatif rejoué à chaque exécution (§6).
Copie pédagogique déclarée (règle organ-first-implementation) : ict/qbf.py porte le module EPITA qbf_native.py (tête a5ac1a5d, commit fondateur 0d2ac1b0, PR EPITA #167), divergences déclarées en docstring — l’acceptabilité sceptique consomme l’organe ict.argumentation au lieu de dung_native ; refus uniformisé accepted=None ; docstrings françaises. Fidélité prouvée par exécution différentielle (16/16 : check_qbf, analyze_qbf, credulous_acceptance_qbf byte-identiques) et 21 gates à littéraux figés. La fonction preferred_extensions est une extension de l’organe natif (pas une copie) : la série demande, l’organe calcule.
Références. Dung, P. M. (1995). On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming, and n-Person Games. Artificial Intelligence 77. · Papadimitriou, C. (1994). Computational Complexity — QBF et la hiérarchie polynomiale. · Pollock, J. (1987). Defeasible Reasoning — le Nixon diamond. · Source distillée : 2025-Epita-Intelligence-Symbolique, argumentation_analysis/agents/core/logic/qbf_native.py.