d4-conf-ecai-2024-0426 (d4-conf-ecai-2024-0426)

Given a shared proposition set \(V\), a finite support of types \(\{(F_t,\mu_t):t\in[\tau]\}\) with \(\mu_t>0\), binary-rational masses summing to \(1\), and a classical query \(Q\), consider policies \(I:V\to\{0,1\}\) satisfying every supported formula \(F_t\) to a finite degree. For each degree \(k\), let \(w_k(I)=\sum_{t:\deg(I,F_t)=k}\mu_t\). Does every policy that lexicographically maximizes \((w_1(I),\ldots,w_K(I))\), where \(K=\max_t\operatorname{opt}(F_t)\), satisfy \(Q\)? If no admissible policy exists, use the paper’s vacuous-entailment convention.

A society is given by its support: a nonempty list of \(\tau\) distinct formula types \(F_t\), each with positive binary-rational mass \(\mu_t\), with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Let \(V\) be the shared proposition set, \(m=|V|\), and \(L\) the total input bit length; express running times in \(m,\tau,L\).
Each \(F_t\) is an explicitly written QCCL formula over \(V\), using \(\neg,\wedge,\vee\), ordered disjunction \(\vec{\times}\), and ordered conjunction \(\vec{\odot}\); the query \(Q\) is a classical propositional formula over \(V\).
Define optionality recursively by \(\operatorname{opt}(a)=\operatorname{opt}(\neg A)=1\), \(\operatorname{opt}(A\wedge B)=\operatorname{opt}(A\vee B)=\max\{\operatorname{opt}(A),\operatorname{opt}(B)\}\), and \(\operatorname{opt}(A\vec{\times}B)=\operatorname{opt}(A\vec{\odot}B)=\operatorname{opt}(A)+\operatorname{opt}(B)\).
For a policy \(I:V\to\{0,1\}\), write \(d_A=\deg(I,A)\) and \(o_A=\operatorname{opt}(A)\). Degrees lie in \(\mathbb Z_{>0}\cup\{\infty\}\), with \(\infty\) larger than every integer: \(\deg(I,a)=1\) when \(I(a)=1\), and \(\infty\) otherwise; \(\deg(I,\neg A)=1\) when \(d_A=\infty\), and \(\infty\) otherwise.
Set \(\deg(I,A\wedge B)=\max\{d_A,d_B\}\) and \(\deg(I,A\vee B)=\min\{d_A,d_B\}\).
Set \(\deg(I,A\vec{\times}B)=d_A\) if \(d_A<\infty\), \(d_B+o_A\) if \(d_A=\infty\) and \(d_B<\infty\), and \(\infty\) otherwise.
Set \(\deg(I,A\vec{\odot}B)=d_B\) if \(d_A=1\) and \(d_B<\infty\), \(d_A+o_B\) if \(d_A<\infty\) and either \(d_A>1\) or \(d_B=\infty\), and \(\infty\) otherwise.
A policy is admissible when every supported formula has finite degree. Put \(K=\max_t\operatorname{opt}(F_t)\) and \(w_k(I)=\sum_{t:\deg(I,F_t)=k}\mu_t\). Preferred policies lexicographically maximize \((w_1(I),\ldots,w_K(I))\) over admissible policies, retaining all ties. Mass entailment asks whether every preferred policy classically satisfies \(Q\); its answer is YES if no admissible policy exists.

Is mass entailment solvable in polynomial time, or is it \(\mathrm{NP}\)-hard?

For finite unweighted theories, an iterative MaxSAT procedure followed by a SAT check correctly decides lexicographic preferred-model entailment ([algorithmic result](https://doi.org/10.3233/FAIA241001)).
Discrete lexicographic entailment is \(\Delta_2^p\)-complete already for QCL and CCL ([complexity result](https://repositum.tuwien.at/bitstream/20.500.12708/142161/1/Bernreiter-2022-Artificial%20Intelligence-vor.pdf)). No result settling exactly the rational-mass formulation was located.

Result

Mass entailment is \(\mathrm{NP}\)-hard under polynomial-time many-one reductions, even when \(\tau=1\), the mass is \(1\), \(K=2\), and every policy is admissible. Consequently, a polynomial-time algorithm would imply \(\mathrm{P}=\mathrm{NP}\).

More precisely, with binary-encoded rational masses, the problem is \(\Delta_2^p=\mathrm{P}^{\mathrm{NP}}\)-complete. We first prove the requested hardness directly, then establish the stronger classification and running-time bounds.

1. A direct reduction from satisfiability

For every classical formula \(A\), the given degree rules imply
\(\deg(I,A)=1\) when \(I\models A\), and \(\deg(I,A)=\infty\) otherwise. This follows by structural induction: atomic degrees encode truth; negation exchanges finite satisfaction and nonsatisfaction; maximum implements conjunction; minimum implements disjunction. Also, \(\operatorname{opt}(A)=1\).

Let \(\varphi\) be an instance of classical propositional satisfiability. Introduce a fresh proposition \(p\), and construct the society and query
\[ F_1=(\varphi\wedge p)\vec{\times}(p\vee\neg p), \qquad \mu_1=1, \qquad Q=p. \]
Here and below, these expressions use exactly the connectives specified in the question.

Both operands of the ordered disjunction are classical and have optionality \(1\). Therefore \(\tau=1\) and \(K=2\). The right operand is always satisfied to degree \(1\), so the ordered-disjunction rule gives
\[ \deg(I,F_1)= \begin{cases} 1,&I\models\varphi\wedge p,\\ 2,&I\not\models\varphi\wedge p. \end{cases} \]
In particular, every policy is admissible.

If \(\varphi\) is satisfiable, some policy satisfies \(\varphi\wedge p\). Its mass vector is \((1,0)\), whereas every policy failing \(\varphi\wedge p\) has vector \((0,1)\). Thus the preferred policies are exactly those satisfying \(\varphi\wedge p\), and all satisfy \(Q=p\). Entailment answers YES.

If \(\varphi\) is unsatisfiable, every policy has vector \((0,1)\). All policies are preferred, including policies setting \(p\) false. Entailment answers NO.

Hence
\[ \varphi\text{ is satisfiable} \quad\Longleftrightarrow\quad \text{the constructed society entails }p. \]
The construction has size linear in the size of \(\varphi\), apart from proposition-name encoding. It is therefore a polynomial-time many-one reduction from SAT, proving \(\mathrm{NP}\)-hardness without using vacuous entailment or any external choice-logic theorem.

2. Polynomial degree bounds and exact mass arithmetic

We establish two facts needed for the upper bound.

Degree bound. Let \(\ell(A)\) denote the number of atomic occurrences in an explicitly written formula \(A\). Then
\[ \operatorname{opt}(A)\leq\ell(A), \qquad \deg(I,A)<\infty\ \Longrightarrow\ \deg(I,A)\leq\operatorname{opt}(A). \]

For the optionality inequality, atoms and negations have optionality \(1\); maximum is bounded by the sum of the operands’ atomic-occurrence counts; and each ordered connective adds optionalities. Structural induction proves the claim.

For the degree inequality, atoms and negations have finite degree \(1\). A finite conjunction degree is the maximum of two finite operand degrees; a finite disjunction degree is bounded by the optionality of a finite operand. For ordered disjunction, the finite result is either \(d_A\leq o_A\) or \(d_B+o_A\leq o_B+o_A\). For ordered conjunction, it is either \(d_B\leq o_B\) or \(d_A+o_B\leq o_A+o_B\). These cases exhaust the rules.

Consequently, \(K=O(L)\). Optionalities can be precomputed, and all degrees for a given policy can be evaluated bottom-up using integers of \(O(\log(L+1))\) bits.

Integer mass representation. Write the binary-encoded input masses as \(\mu_t=p_t/q_t\), with positive integer denominators. Define
\[ D=\prod_{t=1}^{\tau}q_t, \qquad c_t=p_t(D/q_t). \]
Then each \(c_t\) is a positive integer and \(\sum_t c_t=D\). Moreover, \(D\) has \(O(L)\) bits, because its bit length is bounded by the sum of the denominator bit lengths.

For an admissible policy, define
\[ C_k(I)=\sum_{t:\deg(I,F_t)=k}c_t. \]
We have \(w_k(I)=C_k(I)/D\). Thus lexicographically comparing mass vectors is exactly equivalent to comparing the integer vectors \((C_1(I),\ldots,C_K(I))\). Each coordinate belongs to \(\{0,\ldots,D\}\) and has \(O(L)\) bits.

This representation requires no duplication of formulas according to their masses.

3. Membership in \(\Delta_2^p\) and running times

First ask an NP oracle whether an admissible policy exists. A certificate consists of the \(m\) truth values; checking every supported degree takes polynomial time. If no admissible policy exists, return YES as required.

Otherwise, compute the optimal integer profile one coordinate at a time. Suppose the optimal prefix \(b_1,\ldots,b_{k-1}\) has already been found. For an integer threshold \(z\), ask whether there exists an admissible policy \(I\) satisfying
\[ C_j(I)=b_j\quad\text{for every }j<k, \qquad C_k(I)\geq z. \]
This predicate is in NP: guess the policy, evaluate its degrees, and perform the exact integer comparisons.

The threshold predicate is monotone in \(z\). Binary search over \(\{0,\ldots,D\}\) therefore finds the largest feasible value \(b_k\) using \(O(\log(D+1))=O(L)\) oracle calls.

The policies satisfying the optimal prefix remain nonempty at every stage, because each maximum is attained in a finite, nonempty feasible set. After all coordinates are optimized, their vector is the lexicographic maximum. Indeed, a policy differing from it first at coordinate \(k\) must have a smaller \(k\)-th coordinate, by the definition of \(b_k\).

Finally, ask whether there exists an admissible policy satisfying
\[ C_k(I)=b_k\quad\text{for every }k, \qquad I\not\models Q. \]
These are exactly the preferred countermodels. Return NO precisely when this oracle answer is YES.

The procedure uses polynomial deterministic computation and
\(O(1+K\log(D+1))=O(L^2)\) NP-oracle calls. Hence mass entailment belongs to \(\mathrm{P}^{\mathrm{NP}}=\Delta_2^p\).

For an explicit ordinary algorithm, enumerate all \(2^m\) policies, retain the largest profile, and track whether any policy attaining it falsifies \(Q\). Using schoolbook integer arithmetic, a conservative bit-operation bound is
\[ O\!\left(\tau L^2+ 2^m\left[m+L\log(L+1)+(\tau+K)L\right]\right). \]
The first term covers denominator clearing. The terms inside the enumeration cover policy generation, degree evaluation, and integer-profile construction and comparison. Since \(\tau,K=O(L)\), this is also
\[ O\!\left(\tau L^2+2^m(m+L^2)\right). \]
The algorithm uses \(O(m+L^2)\) space and answers YES if enumeration finds no admissible policy.

4. Transfer of the established unweighted hardness

The relevant established theorem is that preferred-model entailment for finite unweighted QCL theories is \(\Delta_2^p\)-complete under lexicographic semantics: admissible policies satisfy every theory formula to finite degree, and preference lexicographically maximizes the counts at successive degrees. These definitions match the present semantics except for replacing counts by masses. See Definition 21 and Proposition 33 of [Bernreiter, Maly, and Woltran, *Choice logics and their computational properties*](https://repositum.tuwien.at/bitstream/20.500.12708/142161/1/Bernreiter-2022-Artificial%20Intelligence-vor.pdf).

We give the reduction explicitly, using only dyadic masses.

Let \(T=\{A_1,\ldots,A_n\}\) be a nonempty unweighted QCL theory, with classical query \(Q\). Choose the smallest power of two \(N\) strictly larger than \(n\). Introduce a fresh proposition \(z\) and the classical tautology \(H=z\vee\neg z\). Construct the support
\[ F_i=A_i,\quad \mu_i=1/N\quad(1\leq i\leq n), \qquad F_{n+1}=H,\quad \mu_{n+1}=(N-n)/N. \]
Every mass is positive and dyadic, and their sum is \(1\). The supported formulas are distinct: the original theory is a set, and \(H\) contains a fresh proposition.

Every policy on the original propositions extends to policies satisfying \(H\), always to degree \(1\). Thus admissibility is preserved under restriction and extension.

For an original policy \(I\), let
\(a_k(I)=|\{i:\deg(I,A_i)=k\}|\).
Every extension \(\widehat I\) has
\[ w_1(\widehat I)=\frac{a_1(I)+N-n}{N}, \qquad w_k(\widehat I)=\frac{a_k(I)}{N}\quad(k\geq2). \]
Adding the same constant to the first coordinate and multiplying every coordinate by the same positive factor preserves every lexicographic comparison, including ties. Therefore the preferred policies of the constructed society are exactly the extensions of the unweighted preferred policies. Since \(Q\) does not mention \(z\), entailment answers agree, including when no admissible policy exists.

The reduction has \(m=m_0+1\), \(\tau=n+1\), and polynomial output length: \(N\leq2n\), so each mass requires \(O(\log(n+1))\) bits. QCL formulas are permitted QCCL formulas with unchanged degrees and optionalities. All hypotheses of the cited hardness theorem therefore apply.

This proves \(\Delta_2^p\)-hardness. Together with Section 3, it establishes \(\Delta_2^p\)-completeness for the rational-mass formulation.

⟨structured verdict parsed — rendered above⟩

Verdict

The output resolves the task correctly. The direct reduction proves \(\mathrm{NP}\)-hardness, including the stated restrictions \(\tau=1\), \(\mu_1=1\), \(K=2\), and universal admissibility. The stronger claim of \(\Delta_2^p\)-completeness is also justified.

No major or minor mathematical issues were found.

1. Direct satisfiability reduction

The preliminary assertion about classical formulas is correct. Structural induction under the supplied rules gives degree \(1\) precisely for satisfying assignments and degree \(\infty\) otherwise. Their optionality is \(1\).

The constructed formula
\[ F_1=(\varphi\wedge p)\vec{\times}(p\vee\neg p) \]
uses a fresh proposition \(p\), so every satisfying assignment of \(\varphi\) extends to one satisfying \(\varphi\wedge p\). Both operands have optionality \(1\), giving \(K=2\).

The degree calculation is exhaustive and correct:

• If \(\varphi\wedge p\) holds, the first operand has degree \(1\), so \(F_1\) has degree \(1\).
• Otherwise, the first operand has degree \(\infty\), while the tautological second operand has degree \(1\). Hence \(F_1\) has degree \(2\).

Every policy is therefore admissible.

When \(\varphi\) is satisfiable, the profile \((1,0)\) is attainable and strictly exceeds \((0,1)\). Exactly the policies satisfying \(\varphi\wedge p\) are preferred, and all satisfy the query \(p\).

When \(\varphi\) is unsatisfiable, all policies have profile \((0,1)\). They are all preferred, including policies falsifying \(p\).

Thus satisfiability corresponds to a YES answer, in the correct direction for a many-one reduction from SAT. The construction has polynomial length and satisfies every input restriction. This independently settles the requested hardness question.

2. Degree bounds and arithmetic

Both structural bounds are valid:
\[ \operatorname{opt}(A)\leq\ell(A), \qquad \deg(I,A)<\infty\Longrightarrow \deg(I,A)\leq\operatorname{opt}(A). \]

For negation, optionality and every finite degree are \(1\); every formula in the specified grammar contains at least one atomic occurrence. For the binary connectives, the stated maximum, minimum, and additive cases preserve the bounds. The ordered-conjunction argument covers both finite-result branches, including the branch where the second operand has infinite degree.

Consequently, \(K=O(L)\), and finite degrees and optionalities require \(O(\log(L+1))\) bits.

Denominator clearing is exact. Since every denominator is positive, \(D/q_t\) is an integer, each \(c_t\) is positive, and normalization gives
\[ \sum_t c_t=D. \]
The product \(D\) has bit length bounded by the sum of the denominator bit lengths, hence \(O(L)\). No numerical magnitude is incorrectly treated as polynomially bounded.

Dividing every coordinate by the same positive \(D\) preserves lexicographic comparisons and ties. The coordinate bounds \(0\leq C_k(I)\leq D\) are also correct.

3. Oracle algorithm

Each oracle predicate is in NP. An assignment provides a certificate; formula evaluation, admissibility checks, integer-coordinate construction, prefix comparisons, and classical query evaluation all take polynomial time.

The initial admissibility test correctly implements the required YES answer when the feasible set is empty.

For each coordinate, threshold feasibility is monotone. The already optimized prefix has a nonempty feasible set, and the next coordinate attains a maximum because there are finitely many policies. Binary search therefore returns the correct coordinate value.

The resulting vector is the lexicographic maximum: at the first coordinate where any admissible policy differs, it cannot exceed the maximum selected subject to the preceding prefix.

The final oracle predicate identifies exactly preferred policies falsifying \(Q\). Reversing its answer is correct for universal entailment.

The oracle-call bound
\[ O(1+K\log(D+1))=O(L^2) \]
is valid, including \(D=1\). Oracle inputs and deterministic intermediate data have polynomial length. Thus membership in \(\mathrm{P}^{\mathrm{NP}}=\Delta_2^p\) is established.

4. Ordinary running time and space

The enumeration algorithm correctly retains the best profile and tracks whether any tied policy falsifies \(Q\). Its empty-feasible-set behavior is specified correctly.

The stated conservative bit-operation bound accounts for denominator clearing, assignment generation, degree evaluation, coordinate accumulation, and profile comparison:
\[ O\!\left(\tau L^2+ 2^m\left[m+L\log(L+1)+(\tau+K)L\right]\right). \]
Classical query evaluation fits within the formula-evaluation allowance.

Since \(\tau,K=O(L)\), the simplified bound follows. Storing the current assignment, formula data, integer weights, and current and best profiles fits within \(O(m+L^2)\) space.

5. Cited hardness theorem and its transfer

The cited source supports the theorem as stated. Definition 21 restricts preference to models satisfying every theory formula and compares counts lexicographically. Proposition 33 establishes \(\Delta_2^p\)-completeness for QCL lexicographic entailment. The surrounding entailment definition uses classical queries, and Definition 5 gives the same QCL connective semantics as the task. Its hardness construction uses nonempty theories. [Bernreiter, Maly, and Woltran, *Choice logics and their computational properties*](https://repositum.tuwien.at/bitstream/20.500.12708/142161/1/Bernreiter-2022-Artificial%20Intelligence-vor.pdf).

The transfer satisfies the relevant restrictions:

• The smallest power of two strictly exceeding \(n\) satisfies \(n<N\leq2n\), so all masses are positive, dyadic, and polynomially encoded.
• The original theory is a set. The additional tautology contains a fresh proposition, ensuring syntactic distinctness.
• The tautology always has degree \(1\), preserving admissibility under restriction and extension.
• Its mass adds the same constant to the first coordinate for every policy; all original counts receive the same positive scaling.
• Consequently, preferences and ties are preserved.
• The query omits the fresh proposition, so entailment is preserved, including vacuous entailment.
• QCL formulas are permitted instances of the supplied QCCL syntax with identical degrees and optionalities.

The reduction therefore establishes the claimed stronger hardness. Combined with the oracle upper bound, it proves \(\Delta_2^p\)-completeness. No clarification or repair is needed.

⟨structured verdict parsed — rendered above⟩