d4-conf-aaai-2024-0116 (d4-conf-aaai-2024-0116)

Given a finite directed cohort graph \(H=(Q,E)\) with positive rational masses \(\mu_q\) summing to \(1\), where each cohort has a shared epistemic state and an activated edge updates the receiving cohort together, and a satisfiable non-tautological target formula \(\varphi\), add a campaign source holding \(\varphi\) with edges to a chosen set \(S\subseteq Q\). What set \(S\) of minimum mass \(\sum_{q\in S}\mu_q\) makes \(\varphi\) unanimously accepted in every admissible run, for every BFN with cohort graph \(H\)?

A society is given by its support: a nonempty list \(Q\) of \(\tau\) cohort types, each with positive binary-rational mass \(\mu_q\), with \(\sum_{q\in Q}\mu_q=1\). Here \(\tau\) is the support size, not the number of possible types. The input also gives a loopless directed graph \(H=(Q,E)\) and a satisfiable, non-tautological propositional formula \(\varphi\) over \(m\) variables; \(L\) is the total input bit length.
Each cohort has one shared epistemic state \(\Psi\), a belief formula \(B(\Psi)\), and its own change operator \(\circ\); initial beliefs are consistent. States and operators are universally quantified, not supplied as input. Define \(\Psi\circ^k\alpha\) by repeated updating and \(\Psi\star\alpha\) as the first positive iterate whose beliefs entail \(\alpha\).
An allowed operator has a bound \(k_\circ\ge1\) such that \(B(\Psi\circ^{k_\circ}\alpha)\models\alpha\) for every state and formula, and satisfies the following conditions for all states and formulas:
\(B(\Psi)\land\alpha\not\models\bot\Rightarrow B(\Psi\star\alpha)\equiv B(\Psi)\land\alpha\); \(\alpha\not\models\bot\Rightarrow B(\Psi\circ\alpha)\not\models\bot\); replacing each input in any finite update sequence by a logically equivalent formula preserves the resulting beliefs up to equivalence.
\(B(\Psi\star\alpha)\land\beta\models B(\Psi\star(\alpha\land\beta))\); if the left side is consistent, the converse entailment also holds.
\((\alpha\models\beta\text{ or }\alpha\models\neg\beta)\Rightarrow B((\Psi\circ\beta)\star\alpha)\equiv B(\Psi\star\alpha)\); \(B(\Psi\star\alpha)\not\models\neg\beta\Rightarrow B((\Psi\circ\beta)\star\alpha)\models\beta\).
Choose whole cohorts \(S\subseteq Q\), costing \(\sum_{q\in S}\mu_q\), and add a source \(c\) with beliefs equivalent to \(\varphi\), no incoming edges, and exactly the outgoing edges \(\{(c,q):q\in S\}\). The source has no society mass or additional cost.
A run activates one augmented edge \((u,v)\) per step and updates only the receiving cohort by \(\Psi_v^{t+1}=\Psi_v^t\circ_v B(\Psi_u^t)\). An admissible run contains every finite word over the augmented edge set as a contiguous block; if that set is empty, the sole run leaves all states constant.
Call \(S\) successful if, for every allowed initial state and operator profile and every admissible run, there exists \(T\) such that \(B(\Psi_q^t)\models\varphi\) for all \(q\in Q\) and \(t\ge T\).

Is computing a successful \(S\) of minimum mass solvable in polynomial time in \(m,\tau,|E|,L\), or is the associated decision problem—whether a successful \(S\) of mass at most a binary-rational budget \(b\in[0,1]\) exists—\(\mathrm{NP}\)-hard?

For finite agents with equal selection costs, a universally successful campaign of minimum cardinality is computable in polynomial time in the graph size. [Source](https://ojs.aaai.org/index.php/AAAI/article/download/28941/29789)
No result addressing exactly the mass-weighted cohort problem above was located.

Result

The minimum-mass campaign is computable in polynomial time. Let $\mathcal C_{\mathrm{src}}$ be the set of source strongly connected components of $H$, meaning components with no incoming edge from another component. Then
$$ S\text{ is successful} \quad\Longleftrightarrow\quad S\cap C\ne\varnothing \text{ for every }C\in\mathcal C_{\mathrm{src}}. $$
Consequently, the optimum mass is
$$ \operatorname{OPT} = \sum_{C\in\mathcal C_{\mathrm{src}}} \min_{q\in C}\mu_q. $$

This graph criterion also appears in Proposition 8 of the [cited paper](https://ojs.aaai.org/index.php/AAAI/article/download/28941/29789). Below is a direct proof for the precise axioms and admissible runs in the question.

1. A consequence of the operator axioms

For a formula $\gamma$, write $[\gamma]$ for its set of satisfying assignments. Fix an allowed operator $\circ$, a state $\Psi$ with consistent beliefs, and a satisfiable input $\beta$. Put
$$ D=B(\Psi), \qquad D'=B(\Psi\circ\beta). $$
The consistency axiom ensures that $D'$ is consistent.

We prove
$$ [D']\subseteq[D]\cup[\beta]. $$
We also prove the stronger statement
$$ D\land\beta\not\models\bot \quad\Longrightarrow\quad D'\equiv D\land\beta. $$

First suppose $D\land\beta$ is consistent. The conjunction axiom for $\star$ gives
$$ B(\Psi\star\top)\equiv D. $$
Thus $B(\Psi\star\top)\not\models\neg\beta$. Applying the final iteration axiom with $\alpha=\top$ yields
$$ B((\Psi\circ\beta)\star\top)\models\beta. $$
Because $D'$ is consistent, the conjunction axiom identifies the left-hand beliefs with $D'$. Hence $D'\models\beta$.

The iteration axiom for $\alpha\models\beta$, applied with $\alpha=\beta$, gives
$$ B((\Psi\circ\beta)\star\beta) \equiv B(\Psi\star\beta). $$
Using the conjunction axiom on both sides, together with $D'\models\beta$, now gives
$$ D'\equiv D\land\beta. $$

Next suppose $D\land\beta$ is inconsistent. Then $D\models\neg\beta$. The iteration axiom for $\alpha\models\neg\beta$, applied with $\alpha=\neg\beta$, gives
$$ B((\Psi\circ\beta)\star\neg\beta) \equiv B(\Psi\star\neg\beta) \equiv D. $$
If $D'\land\neg\beta$ is consistent, the conjunction axiom therefore gives
$$ D'\land\neg\beta\equiv D. $$
If it is inconsistent, $D'\models\beta$. In either case, every model of $D'$ satisfies $D$ or $\beta$, proving the claimed inclusion.

In particular, we have preservation of common entailments:
$$ D\models\varphi,\quad \beta\models\varphi \quad\Longrightarrow\quad D'\models\varphi. $$

Throughout any run, all beliefs remain consistent: initially they are consistent, the source believes the satisfiable formula $\varphi$, and every subsequent input is the consistent belief formula of its sender.

2. Reachability from the source is sufficient

Suppose every cohort is reachable from $c$ in the augmented graph. Fix an arbitrary allowed initial profile and operator profile. For each cohort $q$, choose its uniform bound $k_q$.

Choose a directed spanning tree rooted at $c$. For each cohort $q$, let $p(q)$ be its parent. Process the cohorts in an order in which parents precede children, and form a finite edge word $W$ by concatenating, for each $q$, exactly $k_q$ repetitions of
$$ (p(q),q). $$

We claim that executing $W$ from any consistent profile makes every cohort believe $\varphi$.

During the block for $q$, only $q$ is updated. Its parent is distinct from $q$, so the parent's state stays fixed throughout that block. The parent already believes $\varphi$: this holds initially for $c$ and, inductively, holds for every processed parent. Writing $\beta$ for that fixed parent's belief formula, the uniform bound gives
$$ B(\Psi_q\circ_q^{k_q}\beta)\models\beta\models\varphi. $$
Previously processed cohorts are unchanged during this block. Induction over the tree order proves the claim.

Every admissible run contains $W$ as a contiguous block. Let $T$ be the time immediately after such a block. Then every cohort believes $\varphi$ at time $T$. Every later sender, including $c$, also believes $\varphi$. The preservation result from Section 1 therefore implies, inductively, that
$$ B(\Psi_q^t)\models\varphi \qquad \text{for every }q\in Q\text{ and every }t\ge T. $$

The profile and run were arbitrary. Thus reachability of every cohort from $c$ implies universal success.

3. Missing a source component prevents success

We first construct an allowed operator explicitly, so that the counterexample does not require any additional assumptions about operators.

Let $\Omega$ be the finite set of assignments to the propositional variables. A state consists of a total preorder $\preceq$ on $\Omega$ and a flag $\varepsilon\in\{0,1\}$. Its belief models are
$$ [B(\preceq,\varepsilon)] = \begin{cases} \min_{\preceq}\Omega,&\varepsilon=1,\\ \varnothing,&\varepsilon=0. \end{cases} $$
Every such model set is definable by a propositional formula.

For an input $\alpha$ with model set $A$:

• If $A\ne\varnothing$, put all worlds in $A$ strictly before all worlds outside $A$, preserving the previous ordering within both groups, and set the flag to $1$.
• If $A=\varnothing$, preserve the preorder and set the flag to $0$.

This is lexicographic revision, extended to inconsistent inputs. Its resulting beliefs satisfy
$$ [B(\Psi\circ\alpha)]=\min_{\preceq}A, $$
where the minimum of the empty set is empty. Hence $\star$ is the first update and the uniform bound is $1$.

Here are the checks of all remaining axioms.

• Conjunction when consistent. If the original belief models intersect $A$, the flag is $1$ and

$$ \min_{\preceq}A = \min_{\preceq}\Omega\cap A. $$
This is precisely the required conjunction.

• Consistency and equivalence. A nonempty $A$ has nonempty minima. Updates depend only on model sets, so replacing inputs by equivalent formulas leaves the state, and therefore all resulting beliefs, unchanged.

• The two conjunction entailments. For arbitrary model sets $A,F$,

$$ \min_{\preceq}A\cap F \subseteq \min_{\preceq}(A\cap F). $$
If the left-hand set is nonempty, equality holds: an element of that set witnesses that the minimum rank available in $A\cap F$ equals the minimum rank in $A$. These are exactly the two required entailments.

• The two iteration equalities. If $A\subseteq[\beta]$ or $A\subseteq[\neg\beta]$, updating by $\beta$ preserves the ordering within $A$. Thus its minima, and consequently the beliefs after $\star\alpha$, are unchanged.

• The final iteration entailment. Its antecedent says that

$$ \min_{\preceq}A\cap[\beta]\ne\varnothing. $$
After updating by $\beta$, all $\beta$-worlds precede all other worlds. The minima within $A$ therefore belong to $[\beta]$, as required.

Thus this operator is allowed on its entire state space, including inconsistent states.

Now suppose $C$ is a source strongly connected component of $H$ with $S\cap C=\varnothing$. Since $\varphi$ is non-tautological, choose a world
$$ w_-\models\neg\varphi. $$
Give every cohort initial beliefs whose sole model is $w_-$, and give every cohort the allowed operator just constructed. Such initial beliefs are represented by a preorder with $w_-$ as its unique minimum and flag $1$. The source can likewise be represented with $[\varphi]$ as its minimum class.

There are no incoming edges into $C$ from outside $C$: none from another cohort component because $C$ is a source component, and none from $c$ because $S$ misses $C$.

Inductively, every cohort in $C$ retains the singleton belief model set $\{w_-\}$. Indeed, any update received in $C$ comes from another cohort in $C$, whose input has that same singleton model set. Revision by that input again produces exactly $\{w_-\}$.

Therefore no cohort in $C$ ever believes $\varphi$, and success fails.

For completeness, when the augmented edge set is nonempty, admissible runs exist by concatenating an enumeration of all finite edge words. The counterexample works for every such run. When the edge set is empty, it works for the stipulated constant run.

4. The exact graph criterion

The condensation graph of $H$ is a finite directed acyclic graph. Every component is reachable from a source component: repeatedly following incoming edges backwards must terminate at a source.

If $S$ intersects every source component, then $c$ reaches a selected vertex in each such component. Strong connectivity lets it reach the whole component, and paths in the condensation let it reach every remaining component. Section 2 therefore proves success.

Conversely, if $S$ misses a source component, Section 3 proves failure. This establishes
$$ S\text{ is successful} \quad\Longleftrightarrow\quad S\cap C\ne\varnothing \text{ for every }C\in\mathcal C_{\mathrm{src}}. $$

5. Minimum mass and computational complexity

The source components are disjoint. Every successful $S$ must therefore satisfy
$$ \sum_{q\in S}\mu_q \ge \sum_{C\in\mathcal C_{\mathrm{src}}} \min_{q\in C}\mu_q. $$
Choose a minimum-mass cohort $q_C$ from each source component and set
$$ S^\ast=\{q_C:C\in\mathcal C_{\mathrm{src}}\}. $$
This set is successful and achieves the lower bound, proving the optimum formula.

The algorithm computes the strongly connected components, identifies those with no incoming edge from another component, and chooses a minimum-mass cohort in each. The graph computation takes time
$$ O(\tau+|E|). $$
Comparing the binary-rational masses, summing the chosen masses, and comparing the result with $b$ use exact rational arithmetic with polynomial bit complexity in the total input length.

No model enumeration or propositional satisfiability test is needed; the promised properties of $\varphi$ suffice. Thus both the optimization problem and the associated decision problem are polynomial-time solvable in the requested parameters.

⟨structured verdict parsed — rendered above⟩

The prover resolves the task correctly. The argument establishes the exact success criterion, proves the minimum-mass formula, and gives a polynomial-time algorithm. I found no major or minor issues requiring repair.

1. Consequences of the operator axioms

The consistency assertion for $D'=B(\Psi\circ\beta)$ is justified because $\beta$ is assumed satisfiable.

When $D\land\beta$ is consistent, the conjunction condition applies to $\top$ and gives
$$ B(\Psi\star\top)\equiv D. $$
Consequently, the antecedent of the final iteration condition holds with $\alpha=\top$. Its conclusion is
$$ B((\Psi\circ\beta)\star\top)\models\beta. $$
Since $D'$ is consistent, another application of the conjunction condition identifies these beliefs with $D'$. Thus $D'\models\beta$.

The iteration equality with $\alpha=\beta$ is applicable because $\beta\models\beta$. The conjunction condition applies on both sides: $D\land\beta$ is consistent by hypothesis, and $D'\land\beta$ is consistent because $D'$ is consistent and entails $\beta$. The claimed equality
$$ D'\equiv D\land\beta $$
therefore follows.

When $D\land\beta$ is inconsistent, $D\models\neg\beta$. The iteration equality with $\alpha=\neg\beta$ applies, and the conjunction condition gives
$$ B(\Psi\star\neg\beta)\equiv D. $$
The subsequent case distinction is exhaustive. If $D'\land\neg\beta$ is consistent, the displayed equality with $D$ follows from the conjunction condition. Otherwise, $D'\models\beta$. Both cases establish
$$ [D']\subseteq[D]\cup[\beta]. $$

Preservation of common entailments follows directly from this inclusion. The induction establishing consistency throughout a run is also valid: every sender has consistent beliefs, so every update input is satisfiable.

2. Reachability implies success

The rooted spanning tree exists under the stated reachability hypothesis. Processing parents before children ensures that each parent already entails $\varphi$ when its child’s block begins.

During the block for $q$, only $q$ changes. Its parent is a different vertex, so the input formula remains fixed. The operator’s uniform bound therefore applies to precisely the repeated update sequence written by the prover.

The word $W$ is finite because there are finitely many cohorts and every $k_q$ is finite. Admissibility guarantees an occurrence of this particular word, even though it depends on the fixed operator profile. This respects the required quantifier order: the proof fixes an arbitrary profile and admissible run before obtaining its convergence time.

After the block, preservation of common entailments applies to every subsequent update. The source remains fixed because it has no incoming edges. Thus the proof establishes permanent acceptance, rather than acceptance only at the end of $W$.

3. The counterexample operator satisfies every required axiom

The construction defines an operator on its entire state space. For each input model set $A$, the claimed identity
$$ [B(\Psi\circ\alpha)]=\min_{\preceq}A $$
is correct, including $A=\varnothing$. The resulting beliefs entail $\alpha$, so the first positive update is already $\star\alpha$, and the uniform bound is $1$.

Each remaining check is valid:

• For the conditional conjunction requirement, its antecedent forces the original flag to be $1$. Intersecting the original minimum class with $A$ gives exactly the minima of $A$.
• A nonempty subset of a finite totally preordered set has nonempty minima, establishing consistency for satisfiable inputs.
• Updates depend only on input model sets, establishing equivalence invariance for whole finite sequences.
• The inclusion involving $\min_{\preceq}A\cap F$ has the correct entailment direction. When that intersection is nonempty, the stated minimum-rank argument justifies equality. Empty sets cause no exception.
• If $A$ lies wholly inside $[\beta]$ or wholly outside it, updating by $\beta$ preserves the ordering restricted to $A$. For an inconsistent $\beta$, the construction preserves the whole preorder, so this case is covered as well.
• The antecedent of the final iteration condition is exactly the asserted nonempty intersection. It guarantees that $\beta$ is satisfiable. Promoting its worlds therefore makes every minimum within $A$ a $\beta$-world.

The flag introduces no unhandled inconsistent-state case: after a satisfiable input, the resulting flag is $1$, and after an inconsistent input the resulting beliefs are inconsistent, as required for entailment of that input.

4. Missing a source component prevents success

Non-tautologicity guarantees the existence of $w_-\models\neg\varphi$. The chosen singleton initial beliefs are consistent and are representable by the constructed states. Satisfiability of $\varphi$ likewise permits the stated source representation.

An unselected source component has no incoming augmented edge from outside itself. Every input received inside it therefore has the same singleton model set, and the constructed update preserves that belief set. Hence its cohorts never entail $\varphi$.

The prover also establishes the existence of admissible runs when the edge set is nonempty. Its treatment of the empty edge set agrees with the task’s stipulated constant run. The failure argument therefore does not rely on vacuous quantification over nonexistent runs.

5. Graph characterization and weighted optimum

The condensation argument is valid for every finite nonempty graph, including isolated vertices and singleton components. Meeting every source component gives reachability of every cohort from $c$; missing one gives the counterexample above. Together, these establish the stated equivalence.

Source components are disjoint, and every successful selection must contain a vertex from each. Positive masses justify the lower bound and ensure that selecting additional vertices cannot improve the cost. Choosing one minimum-mass vertex per source component attains the bound. Ties do not affect correctness.

6. Complexity and citation

The graph computation has the stated linear running time. Exact comparisons and sums of binary-rational inputs have polynomial bit complexity in $L$; neither the number of assignments nor the operator bounds enter the selection algorithm. Comparing the optimum with $b$ therefore solves the decision problem in polynomial time.

The satisfiability and non-tautologicity conditions are input promises. The algorithm need not verify them, so omitting a satisfiability test is legitimate.

The attribution to Proposition $8$ is accurate: the [cited paper](https://ojs.aaai.org/index.php/AAAI/article/download/28941/29789) states the corresponding source-component criterion. The present conclusion is independently supported by the direct proof, without importing the paper’s run semantics.

No additional clarification or mathematical repair is needed.

⟨structured verdict parsed — rendered above⟩