# 3.3 — Test de limite : porter τ sur SAT, où aucun ordre n'est donné d'avance.
# On fixe x₁, x₂, x₃ dans cet ordre et on regarde ce que chaque candidat τ
# fait RÉELLEMENT le long de la descente — au lieu de le supposer.
F = [(1, 2, 3), (-1, 2, -3), (1, -2, 3), (-1, -2, -3), (1, 2, -3)]
def clauses_non_satisfaites(clauses, assign):
"""Clauses qu'aucun littéral déjà affecté ne rend vraie."""
return sum(
1 for c in clauses
if not any(abs(l) in assign and assign[abs(l)] == (l > 0) for l in c)
)
descente = [{}, {1: True}, {1: True, 2: True}, {1: True, 2: True, 3: True}]
tau_A = [clauses_non_satisfaites(F, a) for a in descente]
strict_A = [tau_A[i] < tau_A[i - 1] for i in range(1, len(tau_A))]
print("candidat A : τ = clauses non encore satisfaites")
print(f" trajectoire : {tau_A}")
print(f" décroît strictement ? {strict_A} → {all(strict_A)}")
print(" Le dernier pas est PLAT : τ_A décroît, mais pas strictement.")
print(" Elle ne peut donc pas fonder la terminaison.")
tau_B = [3 - len(a) for a in descente]
strict_B = [tau_B[i] < tau_B[i - 1] for i in range(1, len(tau_B))]
print("\ncandidat B : τ = variables non encore affectées")
print(f" trajectoire : {tau_B}")
print(f" décroît strictement ? {strict_B} → {all(strict_B)}")
print(" Elle décroît strictement — mais QUOI QU'IL ARRIVE : elle ne lit jamais F.")
print(" Elle prouve que l'énumération s'arrête, pas que la formule est décidée.")
# Sur 2-SAT, en revanche, le problème FOURNIT l'ordre : les composantes
# fortement connexes du graphe d'implication, et leur condensation est un DAG.
def composantes_fortes(sommets, succ):
"""Kosaraju — composantes fortement connexes, sans dépendance externe."""
vus, ordre = set(), []
for depart in sommets:
if depart in vus:
continue
vus.add(depart)
pile = [(depart, iter(succ.get(depart, ())))]
while pile:
_, it = pile[-1]
for v in it:
if v not in vus:
vus.add(v)
pile.append((v, iter(succ.get(v, ()))))
break
else:
ordre.append(pile.pop()[0])
pred = {}
for a, voisins in succ.items():
for b in voisins:
pred.setdefault(b, []).append(a)
comp, vus2, numero = {}, set(), 0
for depart in reversed(ordre):
if depart in vus2:
continue
vus2.add(depart)
pile, bloc = [depart], []
while pile:
n = pile.pop()
bloc.append(n)
for m in pred.get(n, ()):
if m not in vus2:
vus2.add(m)
pile.append(m)
for n in bloc:
comp[n] = numero # un seul numéro pour TOUT le bloc
numero += 1
return comp
def deux_sat(clauses, nvars):
"""(a ∨ b) ≡ (¬a → b) ∧ (¬b → a) ; satisfiable ssi jamais v et ¬v ensemble."""
succ = {}
for a, b in clauses:
succ.setdefault(-a, []).append(b)
succ.setdefault(-b, []).append(a)
sommets = [s for v in range(1, nvars + 1) for s in (v, -v)]
comp = composantes_fortes(sommets, succ)
ok = all(comp.get(v) != comp.get(-v) for v in range(1, nvars + 1))
return ok, len(set(comp.values()))
print("\n2-SAT : le problème fournit l'ordre (condensation du graphe d'implication)")
for libelle, clauses, nvars in [
("(x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂) ∧ (x₁ ∨ x₂)", [(1, -2), (-1, 2), (1, 2)], 2),
("(x₁ ∨ x₁) ∧ (¬x₁ ∨ ¬x₁)", [(1, 1), (-1, -1)], 1),
]:
ok, n = deux_sat(clauses, nvars)
print(f" {libelle:<38} → {n} composante(s), satisfiable = {ok}")
print("\n τ n'est pas une formule qu'on transporte : c'est un patron qu'on")
print(" CONSTRUIT à partir d'une structure que le problème doit fournir.")
print(" 2-SAT la fournit, et la décision suit. SAT général ne la fournit pas,")
print(" et les deux τ naturelles ci-dessus échouent chacune à leur façon.")