[Rule] Unit ComparativeContainment to DecisionQUBO

Source

ComparativeContainment/weight=One. Given a universe U={0,...,n−1} and indexed
families R=(R_1,...,R_r), S=(S_1,...,S_s) of subsets, find Y⊆U such that
the number of R entries containing Y is at least the number of S entries
containing Y. Empty Y and empty sets are allowed. Repeated family entries
count separately; repeated elements inside a set do not.

The source value is Or; its witness is a Boolean vector of length n.
This proposal concerns unit weights, not the signed weighted variant.

Target

DecisionQUBO/weight=i64, the already registered decision wrapper of QUBO.
Given an upper-triangular quadratic polynomial Q with integer coefficients,
find a Boolean assignment with Q≤b. Each stored coefficient is used once,
not twice. The target value is Or, and completed values map identically.

Motivation

The construction gives the unit containment model a direct quadratic target,
with a rigorously sufficient penalty and exact threshold. The graph at commit
875b6e86d5a87e5f66c2f6743be9d22abe917a09 had no witness path between these
exact variants. An outgoing edge is a solver route, not proof of NP-hardness
of the source.

Model #401
already sketches a linear formulation using containment indicators and their
count difference. That antecedent must be credited. The contribution here is
the explicit product quadratization, sufficient penalty, constant offset,
full-domain equivalence and executable decision-QUBO mapping. No dedicated
proposal for these endpoints was found in the 4,700-record project history
captured on 2026-10-13. Neither that search nor this adaptation claims a new
quadratization theorem in the literature.

Reference

Endre Boros and Aritanan Gruber, On Quadratization of Pseudo-Boolean Functions,
arXiv:1404.6538 (2014), `2.1, equation (4), presenting Rosenberg's product
penalty. The primary full text was read.
The paper supplies the gate technique, not this exact containment rule.

Reduction Algorithm

1. Introduce x_v=[v∈Y] for each v∈U, as the first n target bits.

2. Process R entries then S entries, each in input order. For a set A, list
   its complement a_1<...<a_k. Its exact containment indicator is
   t_A=∏(1−x_{a_j}). For k=0 use constant 1; for k=1 use 1−x_{a_1}.
   For k≥2 use k−1 fresh bits in a chain, first multiplying the first two
   complemented bits, then the preceding result by each remaining factor.

3. For each gate z=ab add the polynomial
   P(a,b,z)=ab−2az−2bz+3z. Its inputs may be bits or complemented bits.

4. Choose M=r+1 and form

   H = M Σ_gates P + Σ_{A in S} t_A − Σ_{A in R} t_A.
   

   Expand and collect coefficients, replacing v² by v. Write H=C+Q, with
   Q containing no constant, and set b=−C. Omit zero coefficients.

5. Validate a target witness against Q≤b once, then return its first n bits.

Gate lemma. At (a,b)=(0,0), P for z=0,1 is respectively 0,3; at (0,1)
and (1,0) it is 0,1; at (1,1) it is 1,0. Thus P≥0 and P=0 iff z=ab.

Forward correctness. Given a feasible Y, fill each chain with its exact
products. Every gate penalty vanishes. The remaining term is the number of S
sets containing Y minus the number of R sets containing Y, hence H≤0 and
Q≤−C.

Backward correctness. For every assignment, even with incorrect gates,
each final indicator is in {0,1}, so the difference of counts is at least −r.
One incorrect gate would imply H≥M−r=1. A target witness has H≤0, so all
gates must be correct. Induction along the chains then identifies every
indicator with actual containment. The threshold is exactly the source
inequality, and extraction is valid without repairing the witness.

Complexity. Let g=Σ_A max(0,n−|A|−1), counting family entries with
multiplicity. Complement enumeration emits O(n(r+s)) gate/indicator records.
Collecting coefficients in a balanced map is polynomial. The mathematical
integer coefficients and offset have polynomial bit length.

Numeric contract. The implementation checks counts and coefficient
arithmetic. A sufficient certificate for every partial target evaluation,
including infeasible assignments, is 8(r+1)g+r+s ≤ i64::MAX. Each expanded
gate contributes at most 8M to the sum of absolute nonconstant coefficients;
indicators contribute at most r+s. The constant also fits that certificate.
Inputs that cannot be represented safely in the fixed-width target return a
typed ReductionError; they are not truncated or silently accepted. This is
an explicit machine-representation limitation, not a restriction hidden in
the mathematical proof.

Size Overhead

The second metric counts stored upper-triangular nonzero entries, including
diagonal terms. Coefficient cancellation can make it smaller. Registered
formulas use universe_size, num_r_sets, num_s_sets; no exact term count
is claimed from these parameters alone.

Validation Method

Local engineering checkpoint. Production code 650a8023 passed fmt,
complete clippy, 6,980 ordinary tests and 149 doctests in a separate retry.
The original Cargo command was interrupted by RAM exhaustion in doctest
compilation, not recorded as exit zero. Test-only HEAD a4b8cba0 changes no
production code and passed fresh fmt (4.566 s), clippy (45.973 s), and all
eight focused rule-05 tests. CLI round trips/default solve, four exporters,
full manual and topology passed. 89 new rule tests were measured below
five seconds: 88 earlier tests (maximum 4.7597 s including startup) plus
the allocation regression (0.017 s). Final new-production coverage PASS:
1,223/1,233 instrumented added lines, 99.189%; every rule exceeds 95%.
The audit excludes 814 added lines with no DA record explicitly; ten
instrumented lines remain uncovered. The focused instrumented extension
passed 8/8 tests. Human scientific review and maintainer approval remain
pending.

All mathematical counts below are local evidence. Proof sources, constructor,
independent adversarial and cross-check scripts are prepared locally and can
accompany a later implementation PR; they are not public certificate URLs.

The preceding proof is the general justification. Finite verification found
no counterexample:

• Constructor: 841,395 assertions in seven nonempty sections, including
  independent source/target evaluation, all small target assignments and
  explicit arithmetic boundaries.
• Fresh-context adversary, given only the proof: 8,580,335 assertions over
  11,637 instance executions; two Hypothesis strategies, 300 examples each,
  seeds 2026101307/2026101308, no persistent database or deadline.
• Cross-comparison: 1,800 identical targets, 18,900 forward checks,
  189,532 target-feasibility checks and 9,423 cross-extractions. The publication
  fixture below was additionally compared and all its 128 target vectors
  examined. Zero disagreements.
• Seven focused Rust tests passed on the first implementation (0.17 seconds),
  including every pair of two-element set families, every target vector for
  those instances, empty universes/families, duplicate elements, gate chains,
  malformed targets, threshold rejection and typed arithmetic errors. The
  improved nonempty canonical fixture is included in the integrated gate.

Example

Take n=4, R=({0,1},{1,2},{1,3}) and S=({0,1,2,3},{0,1,2,3}). Introduce

z0=(1−x2)(1−x3), z1=(1−x0)(1−x3), z2=(1−x0)(1−x2).
H=4[P(1−x2,1−x3,z0)+P(1−x0,1−x3,z1)+P(1−x0,1−x2,z2)] +2−z0−z1−z2.

The constant C is 14, giving bound −14 and seven target bits. The complete
nonconstant polynomial is

Q = −8(x0+x2+x3) +4(x0x2+x0x3+x2x3) −5(z0+z1+z2)
    +8(x2z0+x3z0+x0z1+x3z1+x0z2+x2z2).

There are 15 stored nonzero entries. The source witness Y={1}, or
x=(0,1,0,0), gives z=(1,1,1), all gate penalties zero, H=−1 and Q=−15≤−14.
Extraction returns the same nonempty Y. Flipping one gate bit to zero gives
H=4 and is rejected. The source candidate Y={0,1} is contained in only one R
entry but both S entries; its consistent gate extension has H=1 and is also
rejected.

NO instance. Use the same R but four copies of the full universe in S.
At most three R indicators are one, so every consistent assignment has H≥1;
every inconsistent assignment also has H≥1 by the penalty proof. Here C=16
and the bound is −16. The vector above gives Q=−15, missing the bound by one.

BibTeX

@misc{borosgruber2014quadratization,
  author = {Boros, Endre and Gruber, Aritanan},
  title = {On Quadratization of Pseudo-Boolean Functions},
  year = {2014},
  eprint = {1404.6538},
  archivePrefix = {arXiv},
  primaryClass = {math.OC},
  url = {https://arxiv.org/abs/1404.6538}
}

Attribution and status

Responsible human contributor: Thiago Costa
(@ThiagoCAltoe). Codex AI agents assisted
discovery, proof drafting, implementation and independent automated checking.
Human scientific review is pending. The prior indicator idea in #401 and the
published quadratization method are explicitly acknowledged. Maintainer
acceptance and authorship credit are not claimed.