Navigation : << 15d-Mobius-Coalitions | Index | 16-MechanismDesign >>
Question directrice — Le poids nominal d’un acteur dans un vote pondéré mesure-t-il son pouvoir réel de faire basculer une décision ?
Ce side-track distille le projet T1 d’Ilias Kalalou et Kaelan Grall (EPITA, 2026). Ilias a porté la question, la modélisation des jeux pondérés et les analyses politiques ; Kaelan a porté les définitions des indices, l’encodage Z3, la matrice d’axiomes et les limites. CoursIA ajoute le pont explicite vers le théorème Lean général de Shapley et clarifie la hiérarchie des garanties. Ces ajouts éditoriaux ne sont pas rétro-attribués aux étudiants.
Objectifs
UNSAT comme une vérification bornée et SAT comme un contre-exemple ;Prérequis : coalitions, permutations, logique propositionnelle ; z3-solver. Durée estimée : 55 min.
Environnement chargé : pandas 2.3.3, Z3 4.16.0Un jeu de vote pondéré s’écrit \([q;w_1,\ldots,w_n]\). Une coalition gagne si la somme de ses poids atteint le quota \(q\). Un joueur est critique dans une coalition gagnante si son retrait la rend perdante. Une coalition gagnante est minimale si chacun de ses membres y est critique.
La structure ci-dessous est une réécriture autonome pour CoursIA, fidèle aux concepts et tests du projet d’Ilias Kalalou et Kaelan Grall.
@dataclass(frozen=True)
class VotingGame:
weights: tuple[int, ...]
quota: int
names: tuple[str, ...]
def __post_init__(self):
if len(self.weights) != len(self.names) or not 0 < self.quota <= sum(self.weights):
raise ValueError("Jeu pondéré incohérent")
@property
def players(self):
return range(len(self.weights))
def weight(self, coalition):
return sum(self.weights[i] for i in coalition)
def wins(self, coalition):
return self.weight(coalition) >= self.quota
def coalitions(self):
for size in range(len(self.weights) + 1):
for coalition in combinations(self.players, size):
yield frozenset(coalition)
def minimal_winning(self):
return [s for s in self.coalitions() if self.wins(s) and all(not self.wins(s - {i}) for i in s)]
def is_dummy(self, i):
return all(self.wins(s | {i}) == self.wins(s) for s in self.coalitions() if i not in s)
def is_veto(self, i):
return not self.wins(frozenset(j for j in self.players if j != i))
def is_dictator(self, i):
return self.wins({i}) and self.is_veto(i)
example = VotingGame((3, 2, 1), 4, ("A", "B", "C"))
print("Jeu exemple :", example)
print("Coalitions gagnantes minimales :", [[example.names[i] for i in s] for s in example.minimal_winning()])
print("Rôles :", {
example.names[i]: {
"nul": example.is_dummy(i),
"veto": example.is_veto(i),
"dictateur": example.is_dictator(i),
}
for i in example.players
})Jeu exemple : VotingGame(weights=(3, 2, 1), quota=4, names=('A', 'B', 'C'))
Coalitions gagnantes minimales : [['A', 'B'], ['A', 'C']]
Rôles : {'A': {'nul': False, 'veto': True, 'dictateur': False}, 'B': {'nul': False, 'veto': False, 'dictateur': False}, 'C': {'nul': False, 'veto': False, 'dictateur': False}}Le dictionnaire « Rôles » conclut le diagnostic structurel : aucun joueur nul, aucun dictateur, et un seul véto — A. L’arithmétique du véto est immédiate : sans A, B et C pèsent 2 + 1 = 3, sous le quota de 4 ; aucune coalition ne passe donc sans lui.
Dans [4; 3, 2, 1], les coalitions minimales gagnantes sont {A,B} et {A,C}. A n’est pas dictateur : son poids 3 reste sous le quota. Pourtant, A appartient à toutes les coalitions minimales ; cette structure annonce un pouvoir supérieur à sa seule part de poids.
La dernière hypothèse est le véritable apport absent du corpus CoursIA exécutable avant cette distillation.
def swing_counts(game):
counts = {i: 0 for i in game.players}
for i in game.players:
for s in game.coalitions():
if i not in s and not game.wins(s) and game.wins(s | {i}):
counts[i] += 1
return counts
def power_indices_python(game):
n = len(game.weights)
shapley = {i: 0.0 for i in game.players}
for i in game.players:
others = [j for j in game.players if j != i]
for size in range(n):
coefficient = factorial(size) * factorial(n - size - 1) / factorial(n)
for coalition in combinations(others, size):
s = frozenset(coalition)
shapley[i] += coefficient * (game.wins(s | {i}) - game.wins(s))
swings = swing_counts(game)
absolute = {i: swings[i] / 2 ** (n - 1) for i in game.players}
total = sum(swings.values())
normalized = {i: swings[i] / total for i in game.players}
minimal = game.minimal_winning()
deegan = {i: sum(1 / len(s) for s in minimal if i in s) / len(minimal) for i in game.players}
return pd.DataFrame({
"poids": game.weights,
"part_poids": [w / sum(game.weights) for w in game.weights],
"shapley_shubik": [shapley[i] for i in game.players],
"banzhaf_absolu": [absolute[i] for i in game.players],
"banzhaf_normalise": [normalized[i] for i in game.players],
"deegan_packel": [deegan[i] for i in game.players],
}, index=game.names)
small_python = power_indices_python(example)
print(small_python.round(4).to_string())
print("Sommes :", small_python[["shapley_shubik", "banzhaf_absolu", "banzhaf_normalise", "deegan_packel"]].sum().round(4).to_dict()) poids part_poids shapley_shubik banzhaf_absolu banzhaf_normalise deegan_packel
A 3 0.5000 0.6667 0.75 0.6 0.50
B 2 0.3333 0.1667 0.25 0.2 0.25
C 1 0.1667 0.1667 0.25 0.2 0.25
Sommes : {'shapley_shubik': 1.0, 'banzhaf_absolu': 1.25, 'banzhaf_normalise': 1.0, 'deegan_packel': 1.0}Le tableau croise poids et pouvoir : A porte la moitié du poids (0.5000) mais 0.75 au Banzhaf absolu — trois des quatre coalitions adverses possibles font de lui le joueur décisif — et 0.6667 au Shapley-Shubik. Seconde lecture : B et C affichent les mêmes valeurs sur tous les indices (0.1667 en Shapley-Shubik, 0.25 en Banzhaf absolu) malgré des poids différents — à quota 4, aucune coalition ne les distingue.
La comparaison des indices révèle que Shapley-Shubik et Banzhaf normalisé donnent des résultats similaires, tandis que Deegan-Packel produit une distribution différente (A: 0.50, B: 0.25, C: 0.25).
Les indices normalisés somment à 1, contrairement au Banzhaf absolu. Dans cet exemple, A porte la moitié du poids mais davantage de pouvoir selon chaque expérience. Deegan-Packel accentue la question : il ignore toutes les coalitions gagnantes non minimales, non parce qu’elles seraient impossibles, mais parce que son modèle suppose qu’elles ne sont pas les coalitions pertinentes.
Objectif : compléter une fonction qui retourne les joueurs nuls, à veto et dictateurs d’un jeu.
Indice : utilisez is_dummy, is_veto et is_dictator.
Python parcourait explicitement les sous-ensembles. La voie suivante confie à Z3 les variables booléennes d’appartenance et la contrainte de pivot ou de minimalité. Après chaque modèle, une clause de blocage interdit exactement cette affectation et force le solveur à en trouver une autre.
C’est de l’énumération de modèles SMT, pas du CEGIS : aucune boucle ne synthétise un candidat, ne demande un contre-exemple, puis ne raffine le candidat.
def _models(solver, variables):
found = []
while solver.check() == z3.sat:
model = solver.model()
assignment = tuple(z3.is_true(model.eval(x, model_completion=True)) for x in variables)
found.append(assignment)
solver.add(z3.Or([x != value for x, value in zip(variables, assignment)]))
return found
def swing_sizes_smt(game, player):
others = [i for i in game.players if i != player]
x = [z3.Bool(f"s_{player}_{i}") for i in others]
weight = z3.Sum([z3.If(var, game.weights[i], 0) for var, i in zip(x, others)])
solver = z3.Solver()
solver.add(weight < game.quota, weight + game.weights[player] >= game.quota)
sizes = {}
for assignment in _models(solver, x):
size = sum(assignment)
sizes[size] = sizes.get(size, 0) + 1
return sizes
def minimal_winning_smt(game):
x = [z3.Bool(f"m_{i}") for i in game.players]
weight = z3.Sum([z3.If(x[i], game.weights[i], 0) for i in game.players])
solver = z3.Solver()
solver.add(weight >= game.quota)
for i in game.players:
solver.add(z3.Implies(x[i], weight - game.weights[i] < game.quota))
return [frozenset(i for i, present in enumerate(a) if present) for a in _models(solver, x)]
def power_indices_smt(game):
n = len(game.weights)
by_size = {i: swing_sizes_smt(game, i) for i in game.players}
counts = {i: sum(by_size[i].values()) for i in game.players}
shapley = {i: sum(factorial(k) * factorial(n-k-1) / factorial(n) * count for k, count in by_size[i].items()) for i in game.players}
total = sum(counts.values())
minimal = minimal_winning_smt(game)
deegan = {i: sum(1 / len(s) for s in minimal if i in s) / len(minimal) for i in game.players}
return pd.DataFrame({
"shapley_shubik": [shapley[i] for i in game.players],
"banzhaf_normalise": [counts[i] / total for i in game.players],
"deegan_packel": [deegan[i] for i in game.players],
}, index=game.names), minimal
small_smt, small_mwcs = power_indices_smt(example)
print(small_smt.round(4).to_string())
print("Modèles minimaux Z3 :", [[example.names[i] for i in s] for s in small_mwcs]) shapley_shubik banzhaf_normalise deegan_packel
A 0.6667 0.6 0.50
B 0.1667 0.2 0.25
C 0.1667 0.2 0.25
Modèles minimaux Z3 : [['A', 'B'], ['A', 'C']]Les clauses de blocage ont retrouvé les deux mêmes coalitions minimales que Python. Cette indépendance est relative : les deux voies partagent la définition mathématique du jeu, mais pas le mécanisme d’énumération. Leur accord détecte une classe utile d’erreurs d’implémentation ; il ne transforme pas le calcul en théorème général.
Comparer une seule instance peut masquer une erreur symétrique. Nous croisons donc trois structures : joueur dominant, jeu symétrique et jeu à quatre acteurs.
games = [
VotingGame((3, 2, 1), 4, ("A", "B", "C")),
VotingGame((1, 1, 1), 2, ("X", "Y", "Z")),
VotingGame((5, 3, 2, 1), 6, ("P", "Q", "R", "S")),
]
rows = []
for game_id, game in enumerate(games, 1):
py = power_indices_python(game)
smt, _ = power_indices_smt(game)
for index_name in smt.columns:
rows.append({
"jeu": game_id,
"indice": index_name,
"ecart_max": float((py[index_name] - smt[index_name]).abs().max()),
})
validation = pd.DataFrame(rows)
print(validation.to_string(index=False))
assert validation["ecart_max"].max() < 1e-12
print("Cross-validation réussie : 3 jeux, 3 indices, écart maximal < 1e-12") jeu indice ecart_max
1 shapley_shubik 0.000000e+00
1 banzhaf_normalise 0.000000e+00
1 deegan_packel 0.000000e+00
2 shapley_shubik 0.000000e+00
2 banzhaf_normalise 0.000000e+00
2 deegan_packel 0.000000e+00
3 shapley_shubik 5.551115e-17
3 banzhaf_normalise 0.000000e+00
3 deegan_packel 0.000000e+00
Cross-validation réussie : 3 jeux, 3 indices, écart maximal < 1e-12L’écart affiché est nul à la précision flottante utilisée. Il s’agit d’un test différentiel sur neuf couples jeu/indice, pas d’une preuve universelle. L’espace exploré reste fini et choisi.
Objectif : construire un jeu avec au moins un joueur nul et vérifier que les deux voies lui attribuent un pouvoir nul.
Indice : un petit poids peut être nul si aucun sous-total des autres joueurs ne tombe dans l’intervalle où il ferait franchir le quota.
Exercice 2 à compléter : construire et croiser un jeu avec joueur nulUNSAT prouve quoi ? SAT réfute quoi ?Pour un nombre fixé de joueurs, on peut rendre chaque valeur coalitionnelle \(v(S)\) symbolique, imposer \(v(\varnothing)=0\), \(v(N)=1\), la monotonie et des valeurs binaires. Ajouter la négation d’un axiome permet alors :
UNSAT : aucun jeu dans cet espace borné ne viole la propriété ;SAT : le modèle retourné est un contre-exemple dans cet espace.La cellule vérifie l’efficacité de Shapley-Shubik pour quatre joueurs et demande simultanément à Z3 un contre-exemple à l’efficacité du Banzhaf absolu pour trois joueurs.
def all_subsets(n):
return [frozenset(c) for k in range(n + 1) for c in combinations(range(n), k)]
def simple_game_variables(prefix, n):
subsets = all_subsets(n)
values = {s: z3.Int(f"{prefix}_{sum(1 << i for i in s)}") for s in subsets}
constraints = [values[frozenset()] == 0, values[frozenset(range(n))] == 1]
constraints += [z3.Or(v == 0, v == 1) for v in values.values()]
constraints += [values[s] <= values[s | {i}] for s in subsets for i in range(n) if i not in s]
return subsets, values, constraints
def shapley_expr(values, n, player):
terms = []
others = [i for i in range(n) if i != player]
for k in range(n):
coeff = z3.RealVal(factorial(k) * factorial(n-k-1)) / factorial(n)
for coalition in combinations(others, k):
s = frozenset(coalition)
terms.append(coeff * (values[s | {player}] - values[s]))
return z3.Sum(terms)
def banzhaf_absolute_expr(values, n, player):
others = [i for i in range(n) if i != player]
terms = [values[frozenset(c) | {player}] - values[frozenset(c)] for k in range(n) for c in combinations(others, k)]
return z3.Sum(terms) / z3.RealVal(2 ** (n - 1))
subsets4, v4, constraints4 = simple_game_variables("v4", 4)
proof = z3.Solver()
proof.add(constraints4)
proof.add(z3.Sum([shapley_expr(v4, 4, i) for i in range(4)]) != 1)
subsets3, v3, constraints3 = simple_game_variables("v3", 3)
counterexample = z3.Solver()
counterexample.add(constraints3)
counterexample.add(z3.Sum([banzhaf_absolute_expr(v3, 3, i) for i in range(3)]) != 1)
proof_status = proof.check()
ce_status = counterexample.check()
ce_model = counterexample.model()
winning = [sorted(s) for s in subsets3 if ce_model.eval(v3[s]).as_long() == 1]
print("Efficacité Shapley-Shubik, n=4, négation :", proof_status)
print("Efficacité Banzhaf absolu, n=3, négation :", ce_status)
print("Contre-exemple SAT — coalitions gagnantes :", winning)
assert proof_status == z3.unsat and ce_status == z3.satEfficacité Shapley-Shubik, n=4, négation : unsat
Efficacité Banzhaf absolu, n=3, négation : sat
Contre-exemple SAT — coalitions gagnantes : [[2], [0, 1], [0, 2], [1, 2], [0, 1, 2]]| Résultat | Statut honnête |
|---|---|
| Indices calculés dans les cellules précédentes | calcul exact sur une instance finie |
Négation Shapley UNSAT pour n=4 |
vérification SMT bornée aux jeux simples monotones à quatre joueurs |
Modèle Banzhaf SAT |
contre-exemple général suffisant pour réfuter l’axiome |
Unicité de Shapley dans game_theory_lean/CooperativeGames/Shapley.lean |
théorème formel général du corpus CoursIA |
Le passage du borné au général n’est pas automatique. Le module Lean établit la caractérisation axiomatique de Shapley ; cette explication est un élargissement CoursIA apporté après la soutenance, et non une revendication des étudiants.
Objectif : ajouter à un solveur deux joueurs interchangeables, puis chercher un modèle où leurs valeurs de Shapley-Shubik diffèrent.
Indice : pour chaque coalition ne contenant ni 0 ni 1, contraindre v(S ∪ {0}) == v(S ∪ {1}), puis ajouter l’inégalité des deux expressions.
symmetry_status = None # TODO étudiant : construire le solveur et appeler check().
# Étape 1 : reprendre simple_game_variables.
# Étape 2 : imposer l'interchangeabilité des joueurs 0 et 1.
# Étape 3 : ajouter la négation de l'égalité des indices.
print("Exercice 3 à compléter : statut attendu UNSAT, à vérifier pour n fixé")Exercice 3 à compléter : statut attendu UNSAT, à vérifier pour n fixéIlias Kalalou a étudié les groupes de la XVIIe législature ; nous reprenons ici les effectifs stabilisés à l’automne 2024 cités par le projet source. Le quota est 289 sur 577 sièges. Chaque groupe est traité comme un acteur unitaire — hypothèse forte, explicitement reconnue pendant la soutenance.
Un indice décrit les bascules possibles dans ce modèle. Un vote réel unique ne permet pas d’estimer une fréquence empirique de pivot.
groups = (
("RN", 126), ("EPR", 99), ("LFI", 72), ("SOC", 66),
("DR", 47), ("EcoS", 38), ("DEM", 36), ("HOR", 31),
("LIOT", 23), ("GDR", 17), ("UDR", 16), ("NI", 6),
)
assembly = VotingGame(tuple(w for _, w in groups), 289, tuple(n for n, _ in groups))
assembly_power = power_indices_python(assembly)
print(assembly_power.sort_values("shapley_shubik", ascending=False).round(4).to_string())
print("Contrôle des sièges :", sum(assembly.weights), "; coalitions minimales :", len(assembly.minimal_winning())) poids part_poids shapley_shubik banzhaf_absolu banzhaf_normalise deegan_packel
RN 126 0.2184 0.2459 0.5361 0.2408 0.1020
EPR 99 0.1716 0.1811 0.3838 0.1724 0.0957
LFI 72 0.1248 0.1235 0.2744 0.1232 0.0957
SOC 66 0.1144 0.1126 0.2471 0.1110 0.0910
DR 47 0.0815 0.0761 0.1748 0.0785 0.0965
EcoS 38 0.0659 0.0610 0.1416 0.0636 0.0890
DEM 36 0.0624 0.0571 0.1318 0.0592 0.0863
HOR 31 0.0537 0.0487 0.1123 0.0504 0.0836
LIOT 23 0.0399 0.0351 0.0830 0.0373 0.0799
GDR 17 0.0295 0.0268 0.0635 0.0285 0.0738
UDR 16 0.0277 0.0237 0.0576 0.0259 0.0708
NI 6 0.0104 0.0084 0.0205 0.0092 0.0358
Contrôle des sièges : 577 ; coalitions minimales : 184Le RN, avec 126 sièges, obtient un Shapley-Shubik de 0.2459 et un Banzhaf absolu de 0.5361, montrant que son pouvoir réel dépasse sa proportion simple de sièges (21.84%).
Le classement ne se lit pas comme une consigne politique. Il dépend du quota, de la discipline parfaite supposée des groupes et de l’ensemble des coalitions autorisées. L’écart entre part de sièges et pouvoir modélisé est précisément le phénomène étudié par Ilias Kalalou ; Kaelan Grall en a fourni la lecture comparative par indices.
Le projet étudiant a corrigé son analyse historique afin d’isoler une seule transformation. Nous suivons cette discipline : mêmes 577 sièges, même quota, mêmes autres groupes ; seuls LFI, SOC, EcoS et GDR deviennent un acteur GAUCHE de 193 sièges.
Comparer la somme des pouvoirs avant agrégation au pouvoir du nouvel acteur ne prédit pas un comportement électoral. Cela mesure l’effet structurel de cette unique modification du jeu.
left = {"LFI", "SOC", "EcoS", "GDR"}
bloc_groups = [("GAUCHE", sum(w for n, w in groups if n in left))] + [(n, w) for n, w in groups if n not in left]
bloc_game = VotingGame(tuple(w for _, w in bloc_groups), 289, tuple(n for n, _ in bloc_groups))
bloc_power = power_indices_python(bloc_game)
comparison = pd.DataFrame({
"avant_somme_groupes": assembly_power.loc[list(left), ["part_poids", "shapley_shubik", "banzhaf_normalise", "deegan_packel"]].sum(),
"apres_agregation": bloc_power.loc["GAUCHE", ["part_poids", "shapley_shubik", "banzhaf_normalise", "deegan_packel"]],
})
comparison["ecart_structurel"] = comparison["apres_agregation"] - comparison["avant_somme_groupes"]
print(comparison.round(4).to_string())
print("Invariant contrôlé :", sum(bloc_game.weights), "sièges et quota", bloc_game.quota) avant_somme_groupes apres_agregation ecart_structurel
part_poids 0.3345 0.3345 0.0000
shapley_shubik 0.3239 0.4159 0.0920
banzhaf_normalise 0.3263 0.3874 0.0611
deegan_packel 0.3495 0.1529 -0.1965
Invariant contrôlé : 577 sièges et quota 289Lecture des trois écarts non nuls : Shapley-Shubik passe de 0.3239 à 0.4159 (+0.0920) et Banzhaf normalisé de 0.3263 à 0.3874 (+0.0611) — l’acteur unifié pèse plus que la somme des quatre groupes pris séparément. Deegan-Packel fait le mouvement inverse : 0.3495 → 0.1529 (−0.1965), seul des trois indices à chuter. C’est cohérent avec son hypothèse propre (section 2) : il ne compte que les coalitions gagnantes minimales, dont le paysage est bouleversé par la fusion.
La part de sièges reste identique par construction ; les indices peuvent changer parce que l’ensemble des coalitions et des pivots change. C’est un contrefactuel structurel propre, non une prédiction de vote.
Limites cumulatives : énumération exponentielle ; groupes unitaires ; abstentions, dissidences et alliances improbables absentes ; photographie d’effectifs dépendante de la date ; Deegan-Packel privilégie par hypothèse les coalitions minimales ; aucune causalité politique ne découle des indices.
Le geste d’Ilias Kalalou et Kaelan Grall devient ici un pont en trois étages :
| Outil | Question | Limite |
|---|---|---|
| Énumération Python | quels indices sur cette instance ? | exponentielle |
| Modèles Z3 + blocage | retrouve-t-on pivots et coalitions minimales ? | espace fini |
| UNSAT/SAT borné | existe-t-il une violation pour ce n ? |
pas une preuve pour tout n |
| Lean | le théorème général est-il vérifié par le noyau ? | autre artefact, autre niveau de garantie |
Sources principales : Shapley & Shubik (1954), Banzhaf (1965), Deegan & Packel (1978), Dubey & Shapley (1979), Tang & Lin (2009), de Moura & Bjørner (2008). Provenance détaillée : data/game-theory-15e-coalition-power/SOURCE.md.