# Parameters
BATCH_MODE = "true"Complexity-03c — Naviguer le Zoo exécutable
Navigation : Index | 03 — Plus de temps, plus de problèmes | 03b — Hartmanis–Stearns | 04 — Décider sans connaître la suite →
Inclusions vérifiées sur des instances réelles, oracles jouets séparant deux mondes, carte des non-séparations. Le Complexity Zoo — registre fondé par Scott Aaronson — comme terrain de navigation.
0. Pourquoi ce notebook
Approfondissement du palier 03 — Hiérarchie en temps, compagnon de 03b — Hartmanis & Stearns : après le temps compté et sa hiérarchie stricte, ce carnet prend la carte entière des classes et la fait naviguer. La série se lit par ailleurs 01 — Compter des pas, 02 — Vérifier contre trouver, 04 — Décider sans connaître la suite, 04b — Conjectures online, 05b — Aaronson & Arkhipov et 06 — Déquantification.
Le Zoo recense plus de 500 classes de complexité. Une table d’inclusions recopiée serait une étagère ; ce notebook navigue le Zoo : chaque arête d’inclusion est tournee sur des instances (solveurs reels, temps et memoire mesures), la question des séparations est rendue concrete par des oracles jouets (Baker–Gill–Solovay, deux mondes construits et executes), et la carte des non-séparations se termine sur la barriere qui les protege : la relativisation.
Famille Aaronson (Epic #16781, veine 2) : le Zoo et la Zoo Map sont l’objet pédagogique nommé par le brief — ce carnet en est l’organe d’entrée.
import json
import random as GENERATEUR
import time
from collections import defaultdict
# Toutes les experiences de ce carnet sont deterministes : chaque generateur
# d'instances est execute sous graine fixee, les chronos sont encadres.
GENERATEUR.seed(20260925)
def chrono(fonction, *args, repetitions=3):
durees = []
for _ in range(repetitions):
debut = time.perf_counter()
resultat = fonction(*args)
durees.append(time.perf_counter() - debut)
return resultat, min(durees)
print("Chronometre et generateur severes en place.")Chronometre et generateur severes en place.1. La chaîne des inclusions, tournée sur instances
La ligne du Zoo la plus citée — \(L \subseteq NL \subseteq P \subseteq NP \subseteq PSPACE\) — est d’ordinaire une affirmation. Ici, chaque arête porte un témoin exécutable :
- \(L \subseteq NL\) : l’atteignabilité \(s \leadsto t\) décidée par un vérificateur certicat lu une fois, dont la mémoire de travail hors certificat tient en deux compteurs \(O(\log n)\) — contre le DFS déterministe dont la pile grandit avec le graphe ;
- \(NL \subseteq P\) : le même problème décidé par parcours déterministe, temps mesuré ;
- \(P \subseteq NP\) : 2-SAT (implications + composantes fortement connexes, temps linéaire) contre 3-SAT (DPLL, exponentiel) sur des instances appariées — et le certificat du 3-SAT vérifié en temps polynomial.
# --- 1a. Atteignabilite : le DFS deterministe (P) et sa pile ---
def dfs_atteignable(adj, s, t):
vu = {s}
pile = [s]
pile_max = 1
while pile:
u = pile.pop()
if u == t:
return True, pile_max
for v in adj[u]:
if v not in vu:
vu.add(v)
pile.append(v)
pile_max = max(pile_max, len(pile))
return False, pile_max
def graphe_aleatoire(n, densite=1.5):
adj = defaultdict(list)
for u in range(n):
for _ in range(int(densite)):
v = GENERATEUR.randrange(n)
adj[u].append(v)
return adj
blocs_dfs = []
for n in (40, 100, 250, 600):
adj = graphe_aleatoire(n, 4)
(ok, pile_max), duree = chrono(dfs_atteignable, adj, 0, n - 1)
blocs_dfs.append((n, ok, pile_max, duree))
print(f"n={n:4d} atteint={ok} pile max (espace explore)={pile_max:4d} temps={duree*1e3:8.3f} ms")n= 40 atteint=True pile max (espace explore)= 16 temps= 0.009 ms
n= 100 atteint=True pile max (espace explore)= 35 temps= 0.009 ms
n= 250 atteint=True pile max (espace explore)= 103 temps= 0.039 ms
n= 600 atteint=True pile max (espace explore)= 190 temps= 0.051 msLecture du résultat — le DFS paie son espace
La pile du DFS atteint une fraction de \(n\) : l’algorithme déterministe naturel consomme un espace lineaire. C’est le témoin du contraste qui suit : la même question d’atteignabilité est le problème NL-complet de référence — une machine nondéterministe n’a besoin, elle, que de deviner le chemin sommet par sommet.
# --- 1b. Le verificateur NL : certificat lu UNE fois, deux compteurs en memoire ---
def verificateur_nl(adj, s, t, certificat):
# Memoire de travail hors certificat : u (sommet courant) et pas (compteur).
# Le certificat est un flux parcouru une seule fois, jamais relu.
n = len(adj)
u = s
pas = 0
for v in certificat:
pas += 1
if pas > n + 1:
return False, pas
if v not in adj[u]:
return False, pas
u = v
if u == t:
return True, pas
return u == t, pas
def chemin_temoins(adj, s, t):
# Le "prouveur" (hors machine) : un chemin quelconque s->t, par BFS.
from collections import deque
file = deque([s])
pere = {s: None}
while file:
u = file.popleft()
if u == t:
chemin = []
while u is not None:
chemin.append(u)
u = pere[u]
return chemin[::-1]
for v in adj[u]:
if v not in pere:
pere[v] = u
file.append(v)
return None
print(f"{'n':>5} {'atteint':>8} {'verif NL':>9} {'pas':>5} {'memoire (mots)':>15}")
accord_total = True
for n in (40, 100, 250, 600):
adj = graphe_aleatoire(n, 2.5)
ok_dfs, _ = dfs_atteignable(adj, 0, n - 1)
temoin = chemin_temoins(adj, 0, n - 1)
if temoin is not None:
ok_nl, pas = verificateur_nl(adj, 0, n - 1, temoin[1:])
else:
ok_nl, pas = False, n + 2
accord = ok_dfs == ok_nl
accord_total &= accord
print(f"{n:>5} {str(ok_dfs):>8} {str(ok_nl):>9} {pas:>5} {2:>15} accord={accord}")
print("Accord verificateur/DFS sur toute la famille :", accord_total)
# Un faux temoin : le chemin du dernier graphe, ampute de son arrivee.
# Le verificateur doit le refuser -- c'est la seconde moitie de "exactement".
faux = temoin[1:-1]
ok_faux, _ = verificateur_nl(adj, 0, n - 1, faux)
print("Faux temoin (arrivee amputee) refuse par le verificateur :", ok_faux is False) n atteint verif NL pas memoire (mots)
40 True True 4 2 accord=True
100 True True 9 2 accord=True
250 True True 5 2 accord=True
600 True True 9 2 accord=True
Accord verificateur/DFS sur toute la famille : True
Faux temoin (arrivee amputee) refuse par le verificateur : TrueLecture du résultat — deux mots contre une pile
Le vérificateur accepte les paires atteignables (accord sur les quatre tailles) et refuse le témoin amputé de son arrivée. Sa mémoire de travail — deux mots, indépendants de \(n\) — opposée à la pile du DFS, qui croît avec \(n\) (16, 35, 103 puis 190 sommets empilés sur la famille mesurée), est l’arête \(L \subseteq NL\) rendue visible : même question, mais une mémoire que le DFS paie linéairement là où le vérificateur la paie en deux compteurs — au prix d’un certificat deviné (le nondéterminisme est simulé ici par le prouveur BFS hors machine ; chaque tentative de la machine ne consomme toujours que deux compteurs).
# --- 1c. P contre NP : 2-SAT lineaire, 3-SAT exponentiel, instances appariees ---
import sys
sys.setrecursionlimit(10000) # Kosaraju recursif jusqu'a 2n = 1600 sommets (n = 800)
def deux_sat(clauses, nb_var):
# Kosaraju (recursif, n petit) sur le graphe d'implications : temps lineaire, donc 2-SAT dans P.
n = nb_var
def lit(l): # litteral signe -> index interne : x_i -> i-1, non-x_i -> i-1+n
return abs(l) - 1 if l > 0 else abs(l) - 1 + n
def neg(i):
return i + n if i < n else i - n
adj = [[] for _ in range(2 * n)]
radj = [[] for _ in range(2 * n)]
for (a, b) in clauses:
la, lb = lit(a), lit(b)
adj[neg(la)].append(lb) # (a ou b) = (non-a -> b) et (non-b -> a)
adj[neg(lb)].append(la)
radj[lb].append(neg(la))
radj[la].append(neg(lb))
vu = [False] * (2 * n)
ordre = []
def dfs1(u):
vu[u] = True
for v in adj[u]:
if not vu[v]:
dfs1(v)
ordre.append(u)
for s in range(2 * n):
if not vu[s]:
dfs1(s)
comp = [-1] * (2 * n)
def dfs2(u, c):
comp[u] = c
for v in radj[u]:
if comp[v] == -1:
dfs2(v, c)
c = 0
for s in reversed(ordre):
if comp[s] == -1:
dfs2(s, c)
c += 1
if any(comp[i] == comp[i + n] for i in range(n)):
return False, None
val = {i: comp[i] > comp[i + n] for i in range(n)}
return True, val
def trois_sat_dpll(clauses, nb_var):
# DPLL (propagation de unite + branchement) avec compteur de noeuds explores :
# metrique deterministe -- le temps varie d'une machine a l'autre, pas le nombre
# de noeuds, propriete de l'instance ET de la strategie de branchement.
noeuds = [0]
def resoudre(partiel, restantes):
noeuds[0] += 1
while True:
unitaires = [c[0] for c in restantes if len(c) == 1]
if not unitaires:
break
l = unitaires[0]
nouvelles = []
for c in restantes:
if l in c:
continue
if -l in c:
c2 = [x for x in c if x != -l]
if not c2:
return None
nouvelles.append(c2)
else:
nouvelles.append(c)
restantes = nouvelles
partiel = dict(partiel)
partiel[abs(l)] = l > 0
if not restantes:
return partiel
l = restantes[0][0]
for choix in (l, -l):
cand = [[x for x in c if x != -choix] for c in restantes if choix not in c]
partiel2 = dict(partiel)
partiel2[abs(choix)] = choix > 0
resultat = resoudre(partiel2, cand)
if resultat is not None:
return resultat
return None
solution = resoudre({}, [list(c) for c in clauses])
return solution is not None, solution, noeuds[0]
def verifier_3sat(clauses, solution):
# L'arete P inclus dans NP : verifier un certificat est polynomial.
return all(any((x > 0) == solution.get(abs(x), False) for x in c) for c in clauses)
def instance_2sat(n, m):
clauses = []
for _ in range(m):
a = GENERATEUR.randrange(1, n + 1) * (1 if GENERATEUR.random() < 0.5 else -1)
b = GENERATEUR.randrange(1, n + 1) * (1 if GENERATEUR.random() < 0.5 else -1)
clauses.append((a, b))
return clauses
def instance_3sat_plantee(n, m):
# 3-CNF aleatoire (literal 50/50). Densite 4.6n : juste au-dessus du seuil de
# satisfiabilite 4.267n, la ou les instances aleatoires sont les plus dures pour DPLL.
clauses = []
for _ in range(m):
c = []
while len(c) < 3:
v = GENERATEUR.randrange(1, n + 1)
if v not in [abs(x) for x in c]:
c.append(v if GENERATEUR.random() < 0.5 else -v)
clauses.append(c)
return clauses
def instance_satisfiable(n, m, essais_max=12):
for _ in range(essais_max):
cl = instance_3sat_plantee(n, m)
sat, _, _ = trois_sat_dpll(cl, n)
if sat:
return cl
return cl
# 2-SAT : le probleme de P -- quatre fois plus de variables, ~quatre fois le temps
print("2-SAT (Kosaraju) -- moyenne sur 5 instances :")
for n in (50, 200, 800):
cumul = 0.0
for _ in range(5):
clauses2 = instance_2sat(n, 3 * n)
(sat2, _), d2 = chrono(deux_sat, clauses2, n)
cumul += d2
print(f" n={n:4d} {cumul / 5 * 1e3:8.3f} ms")
# 3-SAT : le probleme NP-complet -- meme question existentielle, densite au seuil
print("3-SAT (DPLL, densite 4.6n) -- moyenne sur 20 instances :")
tailles = (10, 15, 20, 25, 30)
noeuds_moyens = {}
temps_moyens = {}
for n in tailles:
total_noeuds = 0
cumul = 0.0
for _ in range(20):
clauses3 = instance_3sat_plantee(n, int(4.6 * n))
(sat3, sol3, nds), d3 = chrono(trois_sat_dpll, clauses3, n)
total_noeuds += nds
cumul += d3
noeuds_moyens[n] = total_noeuds / 20
temps_moyens[n] = cumul / 20
print(f" n={n:3d} noeuds DPLL : {noeuds_moyens[n]:8.1f} {temps_moyens[n] * 1e3:8.3f} ms")
n0, n1 = tailles[0], tailles[-1]
facteur_noeuds = (noeuds_moyens[n1] / noeuds_moyens[n0]) ** (1.0 / (n1 - n0))
facteur_temps = (temps_moyens[n1] / temps_moyens[n0]) ** (1.0 / (n1 - n0))
print(f"Facteur de croissance par variable ajoutee (noeuds explores, deterministe) : ~{facteur_noeuds:.2f}x")
print(f"Facteur de croissance par variable ajoutee (temps) : ~{facteur_temps:.2f}x")
# L'arete P inclus dans NP, dans l'autre sens : le certificat se verifie en polynomial
certificats = 0
for _ in range(20):
clauses3 = instance_satisfiable(12, 4 * 12)
(sat3, sol3, _), _ = chrono(trois_sat_dpll, clauses3, 12)
if sat3 and sol3 is not None and verifier_3sat(clauses3, sol3):
certificats += 1
print(f"Certificats 3-SAT verifies en temps polynomial par verifier_3sat : {certificats} / 20")2-SAT (Kosaraju) -- moyenne sur 5 instances :
n= 50 0.317 ms
n= 200 1.558 ms
n= 800 4.769 ms
3-SAT (DPLL, densite 4.6n) -- moyenne sur 20 instances :
n= 10 noeuds DPLL : 10.3 0.361 ms
n= 15 noeuds DPLL : 17.6 0.695 ms
n= 20 noeuds DPLL : 23.9 1.494 ms
n= 25 noeuds DPLL : 42.5 4.200 ms
n= 30 noeuds DPLL : 63.9 7.252 ms
Facteur de croissance par variable ajoutee (noeuds explores, deterministe) : ~1.10x
Facteur de croissance par variable ajoutee (temps) : ~1.16x
Certificats 3-SAT verifies en temps polynomial par verifier_3sat : 20 / 20Lecture du résultat — la même question existentielle, deux pentes
2-SAT reste sous quelques millisecondes même à \(n = 800\) : composantes fortement connexes en temps linéaire — un problème de \(P\), quatre fois plus de variables ≈ quatre fois le temps. 3-SAT, sur des instances plus de vingt fois plus petites et tirées à la densité \(4{,}6n\) — juste au-dessus du seuil de satisfiabilité \(4{,}267n\), là où la recherche est la plus dure — paie déjà des millisecondes à \(n = 30\) : chaque variable ajoutée multiplie le coût (facteur de temps mesuré ci-dessus) au lieu de l’ajouter — et le coût par noeud grossit encore, car le nombre de clauses suit \(n\). La pente est modeste à l’échelle jouet, mais elle compose : l’exercice 3 l’extrapole et franchit l’heure de calcul pendant que 2-SAT, lui, aura juste suivi \(n\). L’arête \(P \subseteq NP\) a son témoin dans l’autre sens : verifier_3sat contrôle chaque certificat en un parcours polynomial, quand même le trouver résiste.
2. Deux mondes d’oracles — Baker, Gill & Solovay exécutés
Le Zoo dit ce qui est prouvé (inclusions) et ce qui est ouvert (\(P\) vs \(NP\) en tête). La question naturelle : pourquoi pas une diagonalisation, comme pour la hiérarchie en temps du 03 ? La réponse de Baker–Gill–Solovay (1975) est un exécutable : il existe un oracle \(O\) tel que \(P^O \ne NP^O\), et un oracle \(B\) tel que \(P^B = NP^B\). Deux mondes cohérents — donc aucune technique qui « se relativise » (diagonalisation incluse) ne peut séparer \(P\) de \(NP\) dans le nôtre. Ce paragraphe construit et exécute les deux.
Échelle jouet assumée : chaque machine \(P\) simulée émet au plus \(n\) requêtes d’oracle sur une entrée de taille \(n\) (stand-in borné du polynôme), la machine \(NP\) a droit à l’énumération exhaustive de \(2^n\) témoins. La structure de la preuve — stades, longueurs fraîches, basculement unique — est celle du texte original.
# --- 2a. Monde A : oracle diagonal ou P^O != NP^O ---
def machine_P(oracle, x, defaut=0, budget_marges=0):
# Machine deterministe : parcourt les temoins y de |y| = |x| dans l'ordre lexicographique
# et s'arrete apres n + budget_marges requetes (stand-in du polynome). Repond par vote
# majoritaire, ou par son biais 'defaut' si elle n'a rien vu (elle est arbitraire).
n = len(x)
limite = n + budget_marges
vus = 0
positifs = 0
for entier_y in range(2 ** n):
y = format(entier_y, f"0{n}b")
requete = x + "#" + y
if oracle.get(requete, 0):
positifs += 1
vus += 1
if vus >= limite:
break
if positifs == 0:
return defaut
return 1 if positifs > limite // 2 else 0
def langage_np(oracle, x):
# Cote NP : enumeration exhaustive des temoins (stand-in exponentiel autorise).
n = len(x)
for entier_y in range(2 ** n):
y = format(entier_y, f"0{n}b")
if oracle.get(x + "#" + y, 0):
return 1
return 0
def construire_oracle_separant(nb_machines):
oracle = {}
stades = []
for i in range(1, nb_machines + 1):
# Longueur fraiche : assez grande pour que la machine i (n requetes sur 2^n paires)
# ne puisse pas tout voir, distincte des longueurs precedentes. Biais alterne :
# les machines paires repondent 0 par defaut, les impaires 1 -- les deux types de
# stades (temoin plante / temoin retenu) s'exercent.
n_i = 6 + 2 * i
x_i = format(i, f"0{n_i}b")
reponse_machine = machine_P(oracle, x_i, defaut=i % 2)
if reponse_machine == 0:
# elle dit non : on plante UN temoin -> L_O(x_i) = 1, elle a tort.
y_etoile = format((i * 7919) % (2 ** n_i), f"0{n_i}b")
oracle[x_i + "#" + y_etoile] = 1
stades.append((i, n_i, reponse_machine, 1))
else:
# elle dit oui sans preuve : on ne plante rien -> L_O(x_i) = 0, elle a tort.
stades.append((i, n_i, reponse_machine, 0))
return oracle, stades
ORACLE_A, STADES = construire_oracle_separant(4)
print("Stades de la diagonalisation (machine, taille, reponse machine, valeur reelle) :")
for (i, n_i, rep, reel) in STADES:
verdict = "machine vaincue" if rep != reel else "ERREUR"
print(f" M_{i} : n={n_i:2d} M_i^O(x_i)={rep} L_O(x_i)={reel} -> {verdict}")
separation = all(rep != reel for (_, _, rep, reel) in STADES)
# Verification croisee : le cote NP (exhaustif) lit-il bien L_O ?
accord_np = all(langage_np(ORACLE_A, format(i, f"0{6 + 2*i}b")) == reel
for (i, _, _, reel) in STADES)
print("Toutes les machines P vaincues :", separation)
print("Le temoin exhaustif (cote NP) confirme L_O sur chaque stade :", accord_np)Stades de la diagonalisation (machine, taille, reponse machine, valeur reelle) :
M_1 : n= 8 M_i^O(x_i)=1 L_O(x_i)=0 -> machine vaincue
M_2 : n=10 M_i^O(x_i)=0 L_O(x_i)=1 -> machine vaincue
M_3 : n=12 M_i^O(x_i)=1 L_O(x_i)=0 -> machine vaincue
M_4 : n=14 M_i^O(x_i)=0 L_O(x_i)=1 -> machine vaincue
Toutes les machines P vaincues : True
Le temoin exhaustif (cote NP) confirme L_O sur chaque stade : TrueLecture du résultat — pourquoi la machine perd à chaque stade
Chaque machine \(M_i\) ne voit que \(n_i\) des \(2^{n_i}\) paires \((x_i, y)\) : le basculement d’un seul témoin lui échappe forcément. C’est la mécanique du texte original — stades successifs, longueurs fraîches, un basculement par machine — rendue exécutable : dans ce monde, \(P^O \ne NP^O\), prouvé par construction. L’échelle est jouet, la structure est celle de 1975.
# --- 2b. Monde B : oracle complet ou P^B = NP^B ---
def oracle_qbf(h, x):
# L'oracle (stand-in PSPACE) evalue la formule quantifiee « existe y, h(x, y) »
# par enumeration exhaustive. C'est SON travail : la machine ne paie rien.
n = len(x)
for entier_y in range(2 ** n):
if h(x, format(entier_y, f"0{n}b")):
return 1
return 0
def machine_P_avec_oracle_qbf(x, h):
# La machine P emet UNE requete et recopie la reponse : le langage existentiel
# « existe y, h(x, y) » est lui-meme un QBF a un quantificateur -- une seule question a l'oracle.
return oracle_qbf(h, x), 1
def machine_np_sans_oracle(x, h):
# Le meme langage vu du cote NP SANS oracle : l'enumeration est payee par la machine.
n = len(x)
for entier_y in range(2 ** n):
if h(x, format(entier_y, f"0{n}b")):
return 1
return 0
def h_jouet(x, y):
return x.count("1") + y.count("1") >= len(x)
echantillon = [format(k, "05b") for k in (0, 5, 13, 21, 31)]
accord_b = True
for x in echantillon:
rep_P, requetes = machine_P_avec_oracle_qbf(x, h_jouet)
rep_NP = machine_np_sans_oracle(x, h_jouet)
accord_b &= (rep_P == rep_NP)
print(f"x={x} P^B(x)={rep_P} ({requetes} requete) NP^B(x)={rep_NP} accord={rep_P == rep_NP}")
print("Monde B : la machine P a une requete egale la machine NP exhaustive :", accord_b)x=00000 P^B(x)=1 (1 requete) NP^B(x)=1 accord=True
x=00101 P^B(x)=1 (1 requete) NP^B(x)=1 accord=True
x=01101 P^B(x)=1 (1 requete) NP^B(x)=1 accord=True
x=10101 P^B(x)=1 (1 requete) NP^B(x)=1 accord=True
x=11111 P^B(x)=1 (1 requete) NP^B(x)=1 accord=True
Monde B : la machine P a une requete egale la machine NP exhaustive : TrueLecture du résultat — la barrière de relativisation, vue du jouet
Monde A : \(P^O \ne NP^O\), par construction. Monde B : \(P^B = NP^B\) — le langage existentiel « \(\exists y, h(x,y)\) » est lui-même une formule quantifiée, et une machine \(P\) armée de l’oracle le décide en une requête. Les deux mondes sont cohérents avec les mêmes axiomes : aucune méthode qui se contente de simuler des machines relativisées — la diagonalisation en premier — ne peut donc trancher \(P\) vs \(NP\). C’est la raison pour laquelle la carte du Zoo a un centre ouvert, et pourquoi il a fallu des techniques non relativisantes (arithmétisation, IP = PSPACE) pour les séparations qui ont été prouvées.
3. La carte du Zoo — ce qui est mesuré, ce qui est cité, ce qui est ouvert
Les trois niveaux épistémiques de la série (04b) appliqués à la carte : Mesuré (témoin exécuté dans ce carnet ou dans un sibling), Cité (théorème établi, non rejoué ici), Ouvert (non séparé — et la barrière de relativisation dit pourquoi les oracles n’y suffisent pas).
# --- 3. La carte assemblee depuis les temoins du carnet et de la serie ---
carte = [
# (arete, statut, temoin)
("L incl NL", "Mesure", "verificateur a 2 compteurs contre pile DFS (section 1)"),
("NL incl P", "Mesure", "le meme probleme decide par parcours deterministe (section 1)"),
("P incl NP", "Mesure", "certificat 3-SAT verifie en temps polynomial (section 1)"),
("NP incl PSPACE", "Cite", "un certificat polynomial s'evalue en espace polynomial (tire du socle 01)"),
("P != EXPTIME", "Cite", "theoreme de hierarchie en temps -- rejoue au toy-scale dans 03/03b"),
("P vs NP", "Ouvert", "mondes d'oracles contradictoires (section 2) : la diagonalisation ne tranche pas"),
("NP vs coNP", "Ouvert", "equivaut a : aucun certificateur general pour la non-satisfiabilite"),
("NP vs PSPACE", "Ouvert", "IP = PSPACE (arithmetisation, non relativisante) n'eclaire pas cette arete"),
]
print(f"{'Arete':<16} {'Statut':<8} Temoin")
print("-" * 88)
for arete, statut, temoin in carte:
print(f"{arete:<16} {statut:<8} {temoin}")
completes = sum(1 for c in carte if c[1] == "Mesure")
print(f"\nArêtes à témoin exécutable dans ce carnet : {completes} / {len(carte)}")Arete Statut Temoin
----------------------------------------------------------------------------------------
L incl NL Mesure verificateur a 2 compteurs contre pile DFS (section 1)
NL incl P Mesure le meme probleme decide par parcours deterministe (section 1)
P incl NP Mesure certificat 3-SAT verifie en temps polynomial (section 1)
NP incl PSPACE Cite un certificat polynomial s'evalue en espace polynomial (tire du socle 01)
P != EXPTIME Cite theoreme de hierarchie en temps -- rejoue au toy-scale dans 03/03b
P vs NP Ouvert mondes d'oracles contradictoires (section 2) : la diagonalisation ne tranche pas
NP vs coNP Ouvert equivaut a : aucun certificateur general pour la non-satisfiabilite
NP vs PSPACE Ouvert IP = PSPACE (arithmetisation, non relativisante) n'eclaire pas cette arete
Arêtes à témoin exécutable dans ce carnet : 3 / 8flowchart LR
L[L] --> NL[NL] --> P[P] --> NP[NP] --> PS[PSPACE] --> EX[EXPTIME]
P -.open.- NP
NP -.open.- coNP[coNP]En trait plein : inclusions établies (celles de la section 1 portent leur témoin exécutable ; P ⊊ EXPTIME est la stricte de la hiérarchie en temps, 03). En pointillés : les arêtes ouvertes — chacune résisterait à toute preuve relativisante, comme la section 2 le rend visible.
4. Encart — le gap Mathlib du Zoo
Le même geste que 03b, 05b et 06 : confronter la formalisation du carnet à l’état de Mathlib.
- Ce qui existe : une couche
Computability/réelle — machines de Turing (TuringMachine), fonctions partielles récursives, décidabilité et indécidabilité (Primrec,Partrec, le problème de l’arrêt), réductions many-one. C’est le socle \(L\) de la chaîne, du côté prouvé. - Ce qui n’existe pas (encore) : les classes à bornage — pas de \(\mathrm{TIME}(f)\) paramétrée, pas de \(NP\), pas de \(NL\), pas de machine à oracle, pas de théorème de hiérarchie, pas de Baker–Gill–Solovay. Le Zoo est absent : Mathlib formalise la calculabilité, pas (encore) la complexité.
- Grade : les arêtes de la section 1 sont exécutables (Python mesuré), pas prouvées ; leur formalisation est un programme de recherche ouvert, pas un gap d’encodage. Le jour où Aaronson entre en Lean dans ce dépôt, ce sera par la veine 5 de l’Epic (#16781) — un lake IIT/ICT dédié.
5. Exercices
Exercice 1 — 2-SAT côté NL
L’atteignabilité est NL-complète, et 2-SAT se réduit à l’atteignabilité dans le graphe d’implications. Écrire le vérificateur certicat-lu-une-fois qui décide 2-SAT : le certificat est la suite des sommets d’un chemin dans le graphe d’implications witnessant (ou réfutant) la satisfiabilité, la mémoire de travail reste bornée en \(O(\log n)\) mots.
# Exercice 1 : a completer
def verificateur_2sat_nl(nb_var, clauses, certificat):
# TODO etudiant : decider 2-SAT en lisant le certificat une seule fois,
# memoire de travail bornee (sommet courant + compteur), comme verificateur_nl.
# Le certificat : suite de litteraux (chemin dans le graphe d'implications).
# retour : True/False
return None # TODO etudiant
# Indice : non-a -> b veut dire que si le chemin atteint non-a, il doit passer par b.Exercice 2 — étendre le monde A d’un cran
Une cinquième machine \(M_5\) arrive après coup. Écrire etendre_oracle : un nouveau stade qui choisit une longueur fraîche, simule \(M_5\) sur l’oracle courant, et bascule exactement un témoin pour la vaincre — sans défaire les stades 1 à 4 (les réponses déjà acquises doivent rester fausses pour leur machine).
# Exercice 2 : a completer
def etendre_oracle(oracle, stades, indice_nouvelle_machine=5):
# TODO etudiant : ajouter le stade de la machine indice_nouvelle_machine
# (longueur fraiche n = 6 + 2*indice, simulation, basculement d'UN temoin au plus).
# retour : (oracle_etendu, stades_etendus)
return None, None # TODO etudiant
# Indice : la longueur doit etre nouvelle -- sinon une machine precedente pourrait revoir son temoin.Exercice 3 — projeter la pente du DPLL
La section 1c mesure les noeuds DPLL moyens pour \(n\) croissant et en déduit un facteur de croissance par variable ajoutée. Projeter le temps de résolution attendu à \(n = 40\) puis \(n = 60\), et estimer le plus petit \(n\) où la projection dépasse une heure.
# Exercice 3 : a completer
# facteur_temps et la derniere ligne du tableau 1c (n = 30) sont disponibles.
temps_projete_40 = None # TODO etudiant : projection du temps a n = 40 (secondes)
n_une_heure = None # TODO etudiant : plus petit n ou la projection depasse 3600 s
# Indice : temps(n) ~ temps(30) * facteur_temps ** (n - 30) ; le logarithme retourne n_une_heure.6. Conclusion
| Geste | Où | Ce qui a été mesuré |
|---|---|---|
| Tourner les inclusions | §1 | Atteignabilité décidée deux fois : vérificateur à 2 compteurs contre pile DFS (\(L \subseteq NL\) visible) ; 2-SAT linéaire (\(n = 800\) en milliseconde) contre 3-SAT DPLL à croissance multiplicative par variable (facteur mesuré), certificats vérifiés 20/20 en polynomial |
| Construire les deux mondes | §2 | Oracle diagonal : 4 machines vaincues, témoin exhaustif d’accord (BGS monde A exécuté) ; oracle QBF : la machine \(P\) égale \(NP\) en une requête (monde B) |
| Cartographier honnêtement | §3 | 8 arêtes : 3 à témoin exécuté, 2 citées avec leur origine (hiérarchie 03/03b), 3 ouvertes avec la barrière de relativisation comme raison visible |
| Dater le gap | §4 | Mathlib : calculabilité oui, Zoo non — aucune classe à bornage, aucun oracle ; grade écrit |