Principal-Agent Boolean Games

David Hyland, Julian Gutierrez, Michael Wooldridge · IJCAI 2023 (ijcai23-00017)

mirror found
paperPrincipal-Agent Boolean Games
authorsDavid Hyland, Julian Gutierrez, Michael Wooldridge
venueIJCAI 2023
filed underunclassified
judged bygpt-5.6-luna / xhigh (triple__luna__xhigh__c2r1)
judge confidencemedium
authors would recognise ityes

The anchor — hardness

Theorem 3

A-NASH CONTRACTIBILITY is Σp 3-complete.

statement extracted from the paper’s text layer

Every anchor argued

The continuous mirror question

Given a finite type set \(T\), rational population masses \(\mu\), action sets \(A_t=\{0,1\}^{F_t}\), type goals and costs, observation maps, aggregate threshold objective \(\Phi(x)\), and admissible type-based contracts \(\kappa\), decide whether some \(\kappa\) has a nonempty Wardrop equilibrium set \(\mathrm{NE}_\infty(\kappa)\) and satisfies \(\forall x\in\mathrm{NE}_\infty(\kappa),\ \Phi(x)\), where \(x_{t,a}\ge0\), \(\sum_{a\in A_t}x_{t,a}=\mu_t\), and every action receiving positive mass maximizes its type's contracted utility.

The model it lives in

An atomless population of repeated contractor types, with \(\mu_t\) mass of type \(t\); each type has Boolean actions, goals, costs, and observable projections, while \(x_{t,a}\) records action mass. The principal chooses finite type-based payment tables \(\kappa\), and feasibility—not payment minimization—asks whether all Wardrop equilibria satisfy an aggregate Boolean objective.

The objection that survived

Wardrop equilibria permit a type's mass to split across tied actions, so clearing denominators does not preserve the paper's pure, identity-sensitive equilibria or the \(\exists X_1\forall X_2\exists X_3\) reduction; the proponent acknowledges possible new equilibrium-selection and Class C issues but does not resolve them.

fatal: False

What the mirror covers

The mirror covers Theorems 2 and 3, the two contractibility results; it leaves Proposition 1's verification problems and the structural characterizations in Propositions 2–5, Corollary 1, and Theorem 1 untreated.

Open questions for a prover

The case FOR (proponent)

The strongest mirror is a high-multiplicity population of Boolean-game agents, not a fractionalisation of Boolean variables.

Let \(T\) be a finite set of complete agent types. A type records the agent’s local Boolean variables \(F_t\), observable subset \(O_t\), qualitative goal, cost function, and contract class. The population is a rational mass vector \(\mu\), with \(\mu_t\) the fraction of agents of type \(t\), where \(N\gg |T|\): for example, millions of autonomous contractors drawn from a few dozen recurring role, skill, cost, and audit-interface templates.

Each type-\(t\) agent chooses a discrete action \(a\in A_t=\{0,1\}^{F_t}\). The population state is \(x=(x_{t,a})\), where \(x_{t,a}\) is the mass of type \(t\) choosing \(a\), \(\sum_a x_{t,a}=\mu_t\). Aggregate Boolean conditions, such as “at least \(80\%\) of safety checks are completed”, are represented by rational threshold predicates over \(x\). The principal observes \(a|_{O_t}\), possibly together with finitely many thresholded aggregate audit signals, but not hidden action bits.

A type-level contract is a finite table \(\kappa_t\) paying according to those observations. Utilities retain the paper’s exact lexicographic structure: achieving the qualitative goal dominates cost and payment, while payment then offsets action cost. A population equilibrium is a Wardrop equilibrium: whenever \(x_{t,a}>0\), action \(a\) maximizes type \(t\)’s utility against the population state \(x\). The principal’s objective is a Boolean threshold formula \(\Phi(x)\), and the contract-design question is feasibility, exactly as in the paper rather than payment minimization.

This is a credible high-multiplicity regime. Clearing denominators in \(\mu\) and \(x\) produces a finite population of rational clones, while preserving goals, costs, observations, payments, and aggregate objectives. Boolean actions remain indivisible; only the mass choosing each action is continuous. The contract is type-based because agents with the same complete type are indistinguishable for the model’s purposes.

My lead anchor is Theorem 3, which states that A-NASH CONTRACTIBILITY is \(\Sigma_3^p\)-complete. This theorem is proved in the paper, via a reduction from QSAT3. The corresponding problem is:

Continuum A-Nash Contractibility. Given the finite type system, rational population \(\mu\), cost and goal data, observable structure, and principal objective \(\Phi\), does there exist a finite contract \(\kappa\) such that the population has at least one equilibrium and every equilibrium \(x\in\mathrm{NE}_\infty(\kappa)\) satisfies \(\Phi(x)\)?

Equivalently, the solution is a contract table \(\kappa\) satisfying \( \mathrm{NE}_\infty(\kappa)\neq\varnothing \) and \( \forall x\in\mathrm{NE}_\infty(\kappa),\ \Phi(x) \). This is the natural continuous version of the paper’s requirement that every equilibrium consistent with every possible observation achieve the principal’s goal.

I expect the general Boolean-template version to be Class B: the QSAT3 difficulty lies in the logical agenda, controlled Boolean variables, and universal reasoning over equilibria, rather than in named-agent population counts. Continuization may remove multiplicity-driven hardness, but it does not remove Boolean goal logic or hidden-action strategic structure. The exact classification is an open part of the mirror: allowing genuinely mixed population equilibria may introduce additional continuum-specific support and equilibrium-selection difficulty, potentially producing a Class C component.

The second anchor is Theorem 2, proved in the paper, which states that E-NASH CONTRACTIBILITY is \(\Sigma_2^p\)-complete. Its continuous counterpart is:

Continuum E-Nash Contractibility. Given the same population instance and principal objective \(\Phi\), does there exist a finite contract \(\kappa\) and at least one population equilibrium \(x\in\mathrm{NE}_\infty(\kappa)\) such that \(\Phi(x)\) holds?

A solution is therefore a contract together with a rational equilibrium mass vector witnessing success. This mirrors the paper’s existential contract problem: the principal only needs to create room for one desirable equilibrium. I again expect Class B for succinct Boolean goals, although explicit finite action tables with linear aggregate conditions may fall into Class A through complementarity enumeration or linear/convex programming. That tractable restriction would itself be useful: it would separate the paper’s logical hardness from the population-continuization machinery.

These mirrors cover the paper’s two contract-design results, not every proposition. I would not add Proposition 1 as a third anchor: although it is named and gives \(\Sigma_2^p\)- and \(\Pi_2^p\)-completeness for verification, the paper says those results are readily derived from earlier Boolean-game work, whereas the two contractibility theorems are the paper’s central contributions.

The main further questions are whether contracts should be restricted by a total payment budget, whether the principal should minimize expected payment, how approximate or \(\varepsilon\)-equilibria should be treated, and whether “all equilibria” means literally all support patterns or only equilibria reached by a specified selection rule. A particularly important technical question is whether rational finite populations can be rounded from the continuous equilibrium problem with controlled error.

The weakest point is fidelity to the paper’s original one-shot Boolean game. Its formulas may refer to named agents and individual variables, whereas an atomless population agent has no influence on aggregate predicates. The mirror therefore requires an anonymous, repeated-contractor interpretation in which cross-agent conditions become local templates or aggregate threshold conditions, and contracts cannot discriminate between otherwise identical individuals. That makes this an extension rather than a literal direct mirror. Nevertheless, it preserves the paper’s central object—hidden Boolean actions disciplined by type-dependent lexicographic contracts—and places it in a realistic regime where millions of agents share a small number of complete behavioral types.

The case AGAINST (opponent, writing after the proponent)

I would reject both anchors, though the negative case is narrower here than for most papers: this paper does contain genuine computational results. The problem is that its agents cannot be aggregated without changing the strategic object that those results analyse.

In the paper, an agent is not merely a holder of a goal and a cost function. Agent \(i\) owns a distinct block \(\Phi_i\) of globally named variables, and every goal may refer to every other agent’s variables. The principal’s objective \(\phi\) also refers to that global valuation. Thus identity is operational: changing agent \(i\)’s assignment can affect agent \(j\)’s goal and the principal’s formula. A complete type must therefore include the agent’s position in the global Boolean formula, not just a recurring local template. Cloning such an agent requires private copies of its variables and a new semantics for how the formula refers to all those copies. If the formula is kept intact, the clones are not interchangeable; if it is made anonymous or aggregate-based, one has left the Boolean-game model studied in the paper.

The proposed Wardrop construction exposes the problem. In the atomless limit, one individual has no effect on the aggregate state \(x\). If goals and costs remain local, the game decomposes into independent type-level best-response problems: the population distribution records how many agents choose each action, but it does not reproduce the strategic dependence among Boolean assignments that drives the paper’s equilibria. If goals are instead lifted to aggregate threshold predicates, the result is a new mean-field Boolean game. Away from a threshold, an individual cannot change the predicate at all; at a threshold, the payoff is discontinuous. There is then no general high-multiplicity correspondence between finite pure Nash equilibria and Wardrop equilibria.

Clearing denominators does not repair this. A rational mass vector can be represented by finitely many clones, but a finite clone can change an aggregate threshold by \(1/N\), whereas an atomless agent cannot change it at all. Moreover, Wardrop equilibria permit a type’s mass to split between tied actions. The paper’s equilibria are pure assignments by named agents. These are not two representations of the same solution concept.

This defeats the proposed mirror of Theorem 3. Its reduction encodes

\[ \exists X_1\,\forall X_2\,\exists X_3\,\varphi \]

using three strategically distinguished agents whose variable blocks interact inside the same formula. Replacing them by populations of repeated types does not preserve that quantifier structure. Independent clones can split over assignments, so \(x\) represents fractions of assignments rather than a Boolean valuation. An existential population equilibrium may exploit such a split, while an all-equilibria requirement must quantify over mixtures that have no counterpart in the theorem’s finite game. Adding consensus constraints or coordination incentives could force each mass to choose one assignment, but then the meaningful objects are again a finite collection of macro-agents; the population coordinate has become inert. Adding aggregate coordination instead produces a new game whose complexity and equilibrium semantics are not inherited from Theorem 3.

The same issue is even more severe for Theorem 2. In the proposed E-Nash version, a favourable fractional state \(x\) can be witnessed whenever a type is indifferent between actions and some mixture satisfies \(\Phi(x)\). That is a population-selection phenomenon, not the existence of a desirable pure equilibrium of the paper. If contracts are perturbed to remove such indifference, each type is forced into a deterministic best response and the continuum again contributes only a passive multiplicity. If indifference is retained, the result depends on a new choice about whether arbitrary support mixtures count, whether they are robust, and how they are selected. None of these choices is supplied by the paper.

One could certainly write a respectable new model of anonymous contractors with aggregate safety thresholds, type-level contracts, and Wardrop equilibria. It might even be worth studying. But it would be a mean-field contract-design model inspired by Boolean games, not a high-multiplicity mirror of either theorem, and there is no reliable two-way dictionary back to the paper’s finite instances. The negative case is therefore not airtight: the contractor scenario is a coherent extension. Its weakness is that making it genuinely continuous requires replacing the paper’s identity-sensitive global Boolean game by an anonymous aggregate game; preserving the paper’s game removes the multiplicity, while preserving the multiplicity removes the paper.

The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.