Are Pandemic chain reactions confluent? (vertex spills weight to neighbors at threshold, once)

Question

Are resolutions of chain reactions order-independent in the board game Pandemic? More formally:

You're given an undirected graph $G = (V, E)$ and a vertex weight $w \colon V \to \{0, \ldots, 3\}$. Each vertex is also in a state $s \colon V \to \{\textsf{no outbreak}, \textsf{outbreak}\}$.

To increase a vertex $v$:

• If $s(v) = \textsf{outbreak}$ then nothing happens.
• Else, if $w(v) < 3$ then $w(v) \gets w(v) + 1$.
• Else $s(v) \gets \textsf{outbreak}$ and increase all of $v$'s neighbours.

It is not specified which order $v$'s neighbours should be increased in. Is such a specification superfluous?

I observe that setting $s(v) \gets \textsf{outbreak}$ is essentially the same as removing $v$ from $G$. I don't know how that helps, though.

Also, if I understand what confluence means, I think my question can be stated: "is the following rewriting system confluent?", where each element is a specification of $w$ and $s$ and a number of due increases for each vertex $v$, and each rewrite is an increase of some $v$ (for which an increase is due; also decrement the number of increases due for $v$).

Answer 1

I think you can prove

Let some valid processing sequence be given, and let city $C$ be the city that goes into outbreak as the $n$th city in this sequence. Then in every other processing sequence city $C$ will also go into outbreak at some time.

by long induction on $n$. This means that any two sequences will put the same cities into outbreak, and therefore increase all other cities by the same amount.

Answer 2

Newman's lemma (see also Confluence) states that a rewriting system is confluent if it is terminating and locally confluent. I will apply this to my question.

Let $w$ and $s$ be as in my question, and let $q(v)$ be the number of increments due on $v$ (think "queue").

The following rewrites are then permitted for any $v$:

• $q(v) \gets q(v) - 1$ if $s(v) = \textsf{outbreak}$ and $q(v) > 0$
• $w(v) \gets w(v) + 1$ and $q(v) \gets q(v) - 1$ if $q(v) > 0$ and $w(v) < 3$ and $s(v) = \textsf{no outbreak}$
• $s(v) \gets \textsf{outbreak}$ and $q(v) \gets q(v) - 1$ and $\forall (v, u) \in E: q(u) \gets q(u) + 1$ if $q(v) > 0$ and $w(v) = 3$ and $s(v) = \textsf{no outbreak}$.

(Note that when applying the rules of Pandemic, $s(v)$ is initially $\textsf{no outbreak}$ and $q(v)$ is $0$ for all $v$. I don't think this matters for the proof.)

To show that this is terminating, consider as a termination function $t(s, w, s) = \left(\left|s^{-1}(\textsf{no outbreak})\right|, \Sigma_{\hspace{0.1em}v \in V} \hspace0.25em (3 - w(v)), \Sigma_{\hspace{0.1em}v \in V} \hspace 0.4em q(v)\right)$, i.e. a triple of 1. the number of verticies not in the outbreak state; 2. the capacity at each vertex for absorbing increases without breaking out; 3. the number of due increases. (The triples are ordered lexicographically).

The first rule lowers the third component without increasing any other. The second rule lowers the second component without increasing the first. The third rules decreases the first. Hence, the application of any rule leads to a lexicographically lower value of the triple, and hence the rewriting process terminates. (eventually the third cannot decrease further, at which point the second decreases at least once and the third takes on any value; repeat, hence the second eventually cannot decrease further, etc.).

Next, local confluence, the definition of which is "if $a \to b$ and $a \to c$ then $\exists \, d$ such that $b \to^* d$ and $c \to^* d$", i.e. if I can take the system to two different states in a single rewrite, there is a state reachable from each of $b$ and $c$ (with zero or more rewrites).

Note that in my system, no state allows rewriting at $v$ with more than one rule—i.e. never are two conditions satisfied simultaneously; the single-step rewrite is deterministic at each vertex. Hence if I can rewrite to two different states, it must be by increasing at two different vertices $v$ and $u$.

I will prove that $\textsf{increase(v) then increase(u)}$ leads to the same state as $\textsf{increase(u) then increase(v)}$ for all $u$ and $v$.

Note that the first two rewrite rules only update $q$ and $w$ at the vertex being increased. Hence if the third rule applies to neither $u$ nor $v$ then rewriting at $u$ and $v$ leads to the same state no matter the order of rewrites. (Programmers: notice the similarity with (the absence of) data races.)

So assume the third rule applies to $v$.

If the third rule doesn't apply to $u$ and $u$ is not a neighbor of $v$, once again non-overlapping parts of $(q, w, s)$ are being rewritten, and can be done order-independently.

If the third rule doesn't apply to $u$ and $u$ is a neighbor of $v$, then $q(u)$ is increased by 1 (rule 1 at $v$) and decreased by 1 (rule 1 or 2 at $u$), which clearly commutes; any other rewrites are non-overlapping.

So the last case: rule 3 applies to both $u$ and $v$.

If they are not neighbors and have no shared neighbors, once again non-overlapping parts of $q$, $w$ and $s$ are rewritten, which commutes.

If they are not neighbors but have mutual neighbors $x_i$ for some $i$, then each $q(x_i)$ is twice increased by 1; these two operations clearly commute.

If $u$ and $v$ are neighbors and also have mutual neighbors:

• $q(u)$ and $q(v)$ are both increased and decreased, which commutes.
• $q(x_i)$ is increased twice for each neighbor $x_i$, which commutes.
• all other changes are non-overlapping.

Q. E. D.

Commentary: I observe that $(\{0, \ldots, 3\}, \ge)$ and $(\{\textsf{no outbreak}, \textsf{outbreak}\}, (x \mapsto \textsf{outbreak}))$ are semilattices. A pair of (number of increase-by-1 operations, number of decrease-by-1 operations) with pairwise sum as the join also forms a semilattice with a weird ordering. In the language of CRDTs, these are two increment-only (bounded) counters and a PN counter. Given that Newman's lemma talks of joins, I think this may have helped by avoiding some complexity. Working on some data structure in a semilattice suggests that you might want to look at the join of the two successor states of $a$, but it doesn't automatically prove this $d$ to be reachable via your set of rewrite rules. I guess if there is a rewrite from each element to each greater element the proof is trivial.

Answer 3

This can be argued directly, by considering the directed acyclic graph (DAG) within $(V, E)$ that encodes all of the resulting updates; a directed edge $(u, v)$ corresponds to an outbreak at $u$ that either incremented $w(v)$ or set $s(v) \leftarrow \text{outbreak}$. In this sense, the in-degree of a node corresponds to the number of cubes added (plus one if an outbreak was also triggered). The claim is that any order of updates will always result in a DAG with the same in-degree at each node (i.e., the same number of cubes added, and the same outbreaks).

Assume by way of contradiction that two different orderings result in two DAGs: $D_1 = (V, E_1)$ and $D_2 = (V, E_2)$, with in-degree $\deg^-_{D_1}(v) > \deg^-_{D_2}(v)$ for some $v \in V$. Thus there exists some $u \in V$ such that $e := (u, v) \in E_1$ but $e \not\in E_2$. This can only happen if the parent $u$ had an outbreak in $D_1$ but not in $D_2$ (since $\deg^-_{D_1}(v) > \deg^-_{D_2}(v)$ implies that $D_2$ would have updated $v$ from $u$ if it could). Thus $\deg^-_{D_1}(u) > \deg^-_{D_2}(u)$ as well (since $u$ had an outbreak in $D_1$ but not $D_2$). This argument repeats until we hit the root vertex of $D_1$ (since we are traversing up a directed acyclic path in $D_1$). But the in-degree of the root vertex must be $0$ in both DAGs, a contradiction. $\square$

This could also be turned into an inductive proof to be a bit more formal, but I feel this would only obscure the intuition.

Also note this works for the case of multiple roots as well. In this case we create an imaginary vertex connected to each root (with 3 cubes), and then induce an outbreak at the new root.