d4-conf-atal-2010-0263 (d4-conf-atal-2010-0263)

Given a shared protocol \(\alpha\) with explicit characterisations, a mode \(\sigma\in\{\mathrm{weak},\mathrm{strong}\}\), and a rational distribution \(\mu\) over supported types \(t=(\psi_t,\phi_t)\), what exact mass of the society has a type for which \(\alpha\) matches from \(\psi_t\) to \(\phi_t\) in mode \(\sigma\)?

Fix a propositional vocabulary of \(m\) atoms. Preconditions, postconditions and goals are consistent sets of signed literals, representing conjunctions; entailment in the matching rule means literal-set inclusion. Initial states are sets of positive literals.
A shared protocol \(\alpha\) is supplied with its complete explicit list \(C=\{(P_i,Q_i):1\le i\le n\}\) of path characterisations: \(P_i\) is a path's weakest precondition and \(Q_i\) its maximal postcondition. Characterisation generation is outside the input problem.
A society is given by its support: the list of the \(\tau\) types \(t=(\psi_t,\phi_t)\) with positive mass, each with its mass \(\mu_t\) as a binary rational. Require \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types.
For each type let \(A_t=\{i:P_i\subseteq\psi_t\}\). Weak matching means \(\exists i\in A_t\;Q_i\supseteq\phi_t\); strong matching means \(A_t\ne\varnothing\) and \(\forall i\in A_t\;Q_i\supseteq\phi_t\). Thus strong matching requires an executable terminating outcome.
Given \(\sigma\in\{\mathrm{weak},\mathrm{strong}\}\), the required exact mass is \(M_\sigma=\sum_{t:\,\alpha\text{ matches }t\text{ in mode }\sigma}\mu_t\). Let \(L\) be the total binary input length.

Is computing \(M_\sigma\) solvable in polynomial time, or is it NP-hard? State running times in \(m,\tau,n,L\).

For a single initial-state/goal pair, explicit-characterisation matching has a worst-case bound of \(2n\) entailment operations for either mode; DFS uses \(e+2n\), where \(e\) counts protocol-tree traversals. [Source](https://nms.kcl.ac.uk/peter.mcburney/downloads/pubs/2010/pm-2010-08.pdf)
No prior result settling this exact distribution-over-types mass problem was identified.

Result

For both weak and strong matching, computing the exact mass is polynomial-time solvable.

With literal sets represented by bit vectors, a running-time bound is \(O(\tau n(m+1)+L^2)\) bit operations, including exact rational summation. For ordinary explicit literal-list input, direct comparisons give an alternative bound of \(O(L^2)\), without allocating vectors over the entire vocabulary. These bounds allow an unreduced numerator–denominator output; requiring a reduced fraction still gives polynomial time.

1. Determining which supported types match

For each supported type \(t\) and characterisation \(i\), define Boolean values
\[ \]
\(E_{ti}=[P_i\subseteq\psi_t]\) and \(G_{ti}=[\phi_t\subseteq Q_i]\), where brackets denote the truth value of the enclosed statement.

The definitions in the question give
\[ \]
\(w_t=\bigvee_{i=1}^{n}(E_{ti}\land G_{ti})\)
for weak matching, and
\[ \]
\(s_t=\left(\bigvee_{i=1}^{n}E_{ti}\right)\land\neg\left(\bigvee_{i=1}^{n}(E_{ti}\land\neg G_{ti})\right)\)
for strong matching.

The strong formula explicitly requires at least one executable characterisation. Thus it rejects a type when \(A_t=\varnothing\), including when \(n=0\).

An algorithm scans the characterisations for each type. It checks \(E_{ti}\), and checks \(G_{ti}\) only when \(E_{ti}\) is true. During this scan it records whether there is:

• an executable characterisation;
• an executable characterisation satisfying the goal;
• an executable characterisation failing the goal.

Weak matching holds exactly when the second flag is true. Strong matching holds exactly when the first flag is true and the third is false. These equivalences prove correctness directly from the given matching rules.

There are at most \(2n\) inclusion tests per type, hence at most \(2\tau n\) overall. This also recovers the single-pair operation bound reported in the [cited paper](https://nms.kcl.ac.uk/peter.mcburney/downloads/pubs/2010/pm-2010-08.pdf).

2. Cost of the inclusion tests

Bit-vector representation

Represent a signed-literal set by two vectors of length \(m\), one for positive literals and one for negative literals. Inclusion holds exactly when every set bit of the first set is also set in the second, separately for both signs. Each inclusion test therefore costs \(O(m+1)\) bit operations.

Constructing these vectors costs \(O(L+(n+\tau)(m+1))\). For \(n\geq 1\), the support condition implies \(\tau\geq 1\), so \(n+\tau\leq 2n\tau\). Consequently, preprocessing and matching together cost
\[ \]
\(O(L+\tau n(m+1)).\)

When \(n=0\), both masses are immediately zero.

Explicit literal-list representation

A polynomial bound in \(L\) does not require allocating all \(m\) coordinates.

For literal sets \(U,V\), let \(b(U)\) and \(b(V)\) be their total literal-encoding lengths. Test \(U\subseteq V\) by comparing each literal of \(U\) against the literals of \(V\). Comparing two encoded literals of positive lengths \(a,b\) costs \(O(a+b)\), which is \(O(ab)\). Thus inclusion costs \(O(1+b(U)b(V))\).

Summing the precondition-test costs over all type–characterisation pairs gives
\[ \]
\(O\!\left(n\tau+\left(\sum_i b(P_i)\right)\left(\sum_t b(\psi_t)\right)\right)=O(L^2).\)

The same calculation for the goal tests uses \(\sum_i b(Q_i)\) and \(\sum_t b(\phi_t)\), and also gives \(O(L^2)\). Here every aggregate encoding length is at most \(L\), and \(n,\tau\leq L\) because both lists are explicit.

Hence all matching decisions can be computed in \(O(L^2)\) bit operations, even if many vocabulary atoms never occur in the input.

3. Exact rational summation

Use the standard binary numerator–denominator encoding, writing each mass as \(\mu_t=a_t/b_t\), with positive integers \(a_t,b_t\). Let \(T_\sigma\) be the set of types accepted by the preceding algorithm.

Start with \(N=0,D=1\). For each \(t\in T_\sigma\), replace
\[ \]
\((N,D)\longleftarrow(Nb_t+a_tD,\;Db_t),\)
using the previous values on the right.

Inductively, \(N/D\) equals the sum of the masses processed so far. Therefore the final output is exactly
\[ \]
\(M_\sigma=N/D.\)

It remains to bound the arithmetic cost. At every stage, \(D\) is a product of input denominators, so its binary length is at most
\[ \]
\(1+\sum_t\operatorname{bitlength}(b_t)=O(L).\)

All masses are positive and their total is one. Every partial sum consequently lies in \([0,1]\), giving \(0\leq N\leq D\). Thus the numerator also has \(O(L)\) bits.

Let \(\ell_t\) be the combined binary length of \(a_t,b_t\). Schoolbook multiplication and addition implement one update in \(O(L(\ell_t+1))\) bit operations. Since \(\sum_t\ell_t\leq L\) and \(\tau\leq L\), all updates together cost \(O(L^2)\). The output fraction has \(O(L)\) bits.

If a reduced fraction is required, compute \(\gcd(N,D)\) and divide both integers by it. A straightforward Euclidean implementation gives a sufficient additional bound of \(O(L^3)\): every two remainder steps at least halve the current operand, so there are \(O(L)\) divisions, each costing at most \(O(L^2)\).

4. Conclusion and scope

For either matching mode, the proved bounds are:

| Implementation | Exact fraction output | Reduced fraction output |
|---|---:|---:|
| Bit vectors | \(O(\tau n(m+1)+L^2)\) | \(O(\tau n(m+1)+L^3)\) |
| Direct literal-list comparisons | \(O(L^2)\) | \(O(L^3)\) |

The algorithm examines only the \(\tau\) explicitly supported types and the \(n\) explicitly supplied characterisations. It does not enumerate possible types or generate protocol characterisations. Under precisely these input assumptions, exact mass computation is polynomial-time solvable.

⟨structured verdict parsed — rendered above⟩

The output correctly resolves the task: exact mass computation is polynomial-time solvable for both matching modes under the stated explicit-input assumptions. No substantive gaps or false steps were found.

1. Matching decisions

The definitions
\(E_{ti}=[P_i\subseteq\psi_t]\) and \(G_{ti}=[\phi_t\subseteq Q_i]\)
use the inclusion directions required by the task.

The weak-matching formula
\(w_t=\bigvee_{i=1}^{n}(E_{ti}\land G_{ti})\)
holds exactly when some executable characterisation satisfies the goal.

The strong-matching formula
\(s_t=(\bigvee_{i=1}^{n}E_{ti})\land\neg(\bigvee_{i=1}^{n}(E_{ti}\land\neg G_{ti}))\)
correctly combines existence of an executable characterisation with absence of an executable characterisation that fails the goal. It therefore avoids vacuous acceptance when \(A_t=\varnothing\).

The scan records precisely the information these formulas require. Checking \(G_{ti}\) only when \(E_{ti}\) holds is valid in both modes.

At most two inclusion tests occur per characterisation, giving at most \(2n\) per type and \(2\tau n\) overall. This agrees with the single-pair bound supplied in USER_TASK; correctness does not depend on an external theorem from the linked paper.

2. Representation and matching costs

Bit vectors. Two vectors of length \(m\) correctly represent signed literals. Separate inclusion checks for positive and negative coordinates implement literal-set inclusion in \(O(m+1)\) bit operations.

The preprocessing bound
\(O(L+(n+\tau)(m+1))\)
accounts for reading the input and constructing the vectors. Positive support masses summing to one imply \(\tau\geq1\). When \(n\geq1\), the inequality \(n+\tau\leq2n\tau\) is valid, so preprocessing and matching cost
\(O(L+\tau n(m+1))\).

When \(n=0\), neither matching mode accepts any type, and both masses are zero. Thus this boundary case does not require vector construction.

Explicit literal lists. For positive integer encoding lengths \(a,b\), the inequality \(a+b\leq2ab\) justifies the stated comparison cost \(O(ab)\). Summing over all literal pairs gives the inclusion bound \(O(1+b(U)b(V))\). Empty sets are compatible with this bound: an empty left set is accepted immediately, and an empty right set rejects a nonempty left set immediately.

Summing over type–characterisation pairs gives
\(O(n\tau+(\sum_i b(P_i))(\sum_t b(\psi_t)))\),
and analogously for goal tests. Both are \(O(L^2)\), since the aggregate encoding lengths are bounded by \(L\), and explicit list entries imply \(n,\tau=O(L)\).

This establishes a polynomial bound in total input length even when allocating vectors over all \(m\) atoms would be expensive.

3. Exact rational arithmetic

The update
\((N,D)\leftarrow(Nb_t+a_tD,Db_t)\)
correctly adds \(a_t/b_t\), provided both right-hand expressions use the previous values, as explicitly stated.

The denominator is a product of processed input denominators. Its binary length is bounded by \(1+\sum_t\operatorname{bitlength}(b_t)=O(L)\).

Because accepted masses form a subset of positive masses whose total is one, every partial sum lies in \([0,1]\). Consequently \(0\leq N\leq D\), so the numerator also has \(O(L)\) bits. This argument applies to the unreduced representation as well.

For an input fraction of combined length \(\ell_t\), schoolbook multiplication and addition give the claimed update cost \(O(L(\ell_t+1))\). Summing these costs yields \(O(L^2)\), using \(\sum_t\ell_t\leq L\) and \(\tau=O(L)\). The resulting output has \(O(L)\) bits.

The optional reduction bound is also valid. Euclidean remainder steps decrease operand lengths sufficiently to give \(O(L)\) divisions; schoolbook division of \(O(L)\)-bit integers costs at most \(O(L^2)\) each. Thus \(O(L^3)\) is a sufficient upper bound. A zero numerator presents no difficulty because \(D>0\).

4. Scope and verdict

The argument uses exactly the supplied support and complete characterisation list. It does not assume that characterisations can be generated efficiently or that all possible types can be enumerated efficiently.

The final bounds follow:

• Bit vectors: \(O(\tau n(m+1)+L^2)\) for an exact unreduced fraction; \(O(\tau n(m+1)+L^3)\) with reduction.
• Explicit literal lists: \(O(L^2)\) for an exact unreduced fraction; \(O(L^3)\) with reduction.

The case \(m=0\), empty goals, empty literal sets, and no accepted types are all covered by the same definitions and algorithm.

No mathematical repair or additional clarification is required.

⟨structured verdict parsed — rendered above⟩