NP-completeness of deciding non-zero `HAVING` provenance #

Deciding whether the provenance of a HAVING SUM query over an ℕ[X]- or 𝔹[X]-instance is non-𝟘 is NP-complete, already in data complexity: the query SELECT DISTINCT 1 FROM R GROUP BY b HAVING SUM(v) = b is fixed and only the instance varies.

The development is in three parts.

The bridges (havingSumProv_ne_zero_iff, havingSumProvBool_ne_zero_iff): over ℕ[X] = MvPolynomial X ℕ and over 𝔹[X] = BoolFunc X, with pairwise distinct variables as annotations, the possible-world provenance of SUM(t) = B on a group U is non-𝟘 exactly when some non-empty W ⊆ U satisfies ∑ i ∈ W, t i = B. Over ℕ[X] the monus factor of a world annotation collapses to 𝟙 and the surviving monomials are pairwise distinct, so no cancellation occurs; over 𝔹[X] the valuation realizing exactly the occurrences of a witnessing world satisfies the provenance, whose satisfiability is non-𝟘-ness.
The complexity half: that combinatorial condition, read off a Language.binWeights structure, is a decision problem HavingSumNonzero, and it is NP-complete. Hardness is an FO reduction from Knapsack (subset-sum with binary weights), so it is stronger than a Karp reduction.
The encoding half, which joins the two: a concrete group is a list of aggregate values and a constant, encoded by DescriptiveComplexity.binarySubsetSumEncoding, whose declared size is the total bit length and whose no-padding/no-compression bounds are discharged at construction. havingSumNonzeroHow_faithful and havingSumNonzeroBool_faithful prove that HavingSumNonzero computes exactly non-zero provenance on every encoded group, and exists_concreteNonemptySubsetSum_iff – through the computable decoder of DescriptiveComplexity.bwDecode – that every structure is such a group, so both halves of the NP-completeness below are statements about concrete groups.

That last half is not bookkeeping. Values written in unary would make the problem tractable – Provenance.Algorithms.SumDP is the very dynamic program that solves it, and DescriptiveComplexity.no_unary_encoding shows the size bounds reject that reading – so the representation is part of the statement, and the encoding is where it is pinned down.

Hardness is a padding interpretation: keep the instance and add one weight-zero item per element of the universe. Those items change no reachable total, but they make a solution non-empty, which is what the possible-world semantics requires: Having.havingProv sums over the non-empty sub-worlds of a group only.

Main results #

havingSumProv_ne_zero_iff, havingSumProvBool_ne_zero_iff – the two bridges;
HavingSumNonzero – the bundled decision problem;
hasNonemptySubsetSum_iff – it is Knapsack cut down by one FO sentence;
knapsack_fo_reduction_havingSumNonzero – the padding FO reduction;
havingSumNonzero_NP_complete – NP-completeness, in data complexity;
havingSumNonzeroHow_faithful, havingSumNonzeroBool_faithful – the encoding of concrete groups is faithful, which carries membership to concrete groups;
havingSumNonzeroDecoding and exists_concreteNonemptySubsetSum_iff – the computable decoding back, which carries hardness: the problem is nowhere hard on structures that are not groups.

NP-completeness of deciding non-zero HAVING provenance #

Main results #

Step 1: the provenance of a HAVING SUM predicate #

Step 2: ℕ[X] with distinct variables – no cancellation #

Step 2': 𝔹[X] with distinct variables – the same characterization #

Step 3: the decision problem and its membership in NP #

Step 4: NP-hardness, by FO reduction from Knapsack #

Step 5: the concrete groups the theorem is about #

Step 6: reading the hardness back on concrete groups #

NP-completeness of deciding non-zero `HAVING` provenance #

Step 1: the provenance of a `HAVING SUM` predicate #

Step 2: `ℕ[X]` with distinct variables – no cancellation #

Step 2': `𝔹[X]` with distinct variables – the same characterization #

Step 4: NP-hardness, by FO reduction from `Knapsack` #