[Rule] IntegerExpressionMembership to binary ILP #1198

Source

IntegerExpressionMembership (no variant parameters).

An input is a binary tree of positive i64 singleton atoms, union nodes and Minkowski-sum nodes, with a positive i64 target K. A witness makes branch choices so the active expression evaluates to K. Actual types are Problem::Solution = Vec<bool> and Problem::Value = Or.

The evaluator consumes a bit only when it visits a union in active depth-first, left-before-right order. Unvisited subtrees consume no bits. The supplied witness nevertheless has one coordinate for every union in the full tree; unused trailing coordinates are ignored. The proposed decoder follows this actual behavior.

Target

ILP<bool,i64> — registered variant ILP/variable=bool/coefficient=i64/bounds=general.

Every variable is binary, and the objective is constant-zero minimization. Target types are Solution = Vec<i64> and Value = Extremum<i64>. Use the library's explicit ilp_feasibility completed-value map and validate target feasibility before extraction.

Motivation

This turns recursive integer-set membership into a polynomial-size binary ILP without expanding the potentially exponential set of represented integers. Activations preserve the tree structure; binary full adders keep coefficients small even at the signed-i64 boundary.

The model discussion in #552 states that a natural ILP encoding would need exponentially many constraints to capture the recursive set structure and does not plan an outgoing ILP rule. The construction below gives a polynomial encoding of that structure. No dedicated rule with these endpoints was found in the all-state issues/PR history captured on 2026-10-13. This does not establish global novelty.

Reference

The direct construction and proof are self-contained below. Binary adders and activation constraints are established encodings; no globally new arithmetic theorem is claimed.

Background inspected: Fred Glover, Improved Linear Integer Programming Formulations of Nonlinear Integer Problems, Management Science 22(4), 455–460 (1975), section 3, on binary expansion. Author-hosted primary PDF. The paper is background; it is not asserted to contain this exact expression-membership rule.

Reduction Algorithm

Let A be the atom count, S the sum-node count, U the union-node count and T=2A−1 the total node count. Number nodes in preorder and atoms v_1,…,v_A from left to right. Let H be the largest binary length of K and all atom values, so 1≤H≤63. Write v_{j,b} for bit b of atom j, with bits numbered from zero.

1. Introduce binary node activations a_t, with the root fixed to one. For a sum node t with children l,r, require a_l=a_t and a_r=a_t. For a union node, require a_l+a_r=a_t.

2. For every atom j, introduce H prefix bits p_{j,b} and H−1 carry bits c_{j,b} for 1≤b<H. Omitted constants are p_{0,b}=0, c_{j,0}=0, and c_{j,H}=0. Coordinates are all activations, then atom-major/bit-minor prefix bits, then atom-major/bit-minor carry bits.

3. Add, for every atom and bit, the equation

   p_{j−1,b} + v_{j,b} a_{v_j} + c_{j,b} − p_{j,b} − 2c_{j,b+1} = 0.
   

   Omit the defined constant-zero symbols and zero-coefficient terms. The omitted final carry forbids arithmetic overflow beyond bit H−1.

4. Fix final prefix bits p_{A,b} to the corresponding bits of K. Minimize zero.

5. After feasibility validation, traverse the active tree: at a sum visit left then right; at a union append its chosen branch bit and visit only that child. Append false bits at the end until length U; these are the explicit unused-tail sentinel, not repairs to a malformed solution.

Arithmetic lemma. Multiply each bit equation of stage j by 2^b and sum over all bits. Internal carry terms cancel, and the boundary carries are zero, giving the exact identity P_j=P_{j−1}+v_j a_{v_j}, where P_j=Σ_b 2^b p_{j,b}. Conversely, whenever that addition is below 2^H, ordinary binary addition supplies bits satisfying all equations. At each bit the result bit and outgoing carry are uniquely determined, proving uniqueness of arithmetic auxiliaries, including H=1 with no internal carries.

Correctness, forward. A source witness defines its active evaluation tree. Every visited sum activates both children; every visited union activates exactly its chosen child; all descendants of an inactive node remain inactive. The active atom values sum to K. Because all atoms are positive, every left-to-right prefix total lies in [0,K] and fits H bits. The arithmetic lemma supplies a feasible binary extension and the final prefix equals K.

Correctness, backward. A feasible activation assignment gives an active root, both children at every active sum, and exactly one child at every active union. An inactive node forces its descendants inactive. Summing the arithmetic identities gives Σ_j v_j a_{v_j}=P_A=K. Reading the active DFS choices therefore produces a source expression with value K. Positivity and K≤2^63−1 imply that every partial sum encountered by source evaluation is representable, so the extracted witness cannot fail because of source checked_add overflow.

Complexity and arithmetic. Construction uses O(T+AH) time and storage. Every coefficient is in {-2,-1,0,1}, every right-hand side in {0,1}, and the absolute row evaluation is at most five even on infeasible binary assignments. Counts and indices are checked. Large atom values are represented by bits, not by large row coefficients.

Size Overhead

Let B=Σ_j popcount(v_j).

The nonzero count includes the root (1), sum-node rows (4S), union-node rows (3U), previous-prefix terms (H(A−1)), atom bits (B), both directions of internal carry use (2A(H−1)), current-prefix terms (AH) and final bits (H). Row indices are distinct, so normalization removes no nonzero term.

Registry limitation: the source currently registers only num_union_nodes = U. Arbitrarily large sum-only trees have U=0, so no valid size formula for the first three target parameters can be expressed using that registered parameter alone. Those transform fields are explicitly unavailable, with that reason; the magnitude-bit upper bound is 2. This metadata limitation does not weaken the polynomial bound in the actual encoded tree and atom bit lengths. The rule does not expand the source model merely to manufacture parameter formulas.

Validation Method

The proof establishes the general result. Finite tests search for counterexamples and check implementations.

• Constructor audit: 9,570 instance executions, 130,421 assertions, seed 2026101302. It exhausts full binary trees of up to five nodes with atom values 1–3 and targets 1–10, samples 300 cases per documented (U,S) cell, enumerates feasible target extensions and small raw Boolean domains, and covers signed-i64 extremes and active DFS decoding. All seven required sections passed.
• Fresh-context adversary given only the Typst proof: 12,945 instance executions, 934,209 assertions, seeds 2026101303 and 2026101304, two Hypothesis strategies with 300 examples each, database=None, deadline=None; zero failed assertions. Construction, extraction and checkers were independently reimplemented.
• Cross-comparison: 105 identical target constructions after documented sparse-term normalization, 3,150 target-feasibility comparisons, 8 cross-extractions and 428 source-config comparisons; zero disagreements.
• Rust focused tests: 8 passed, 0 failed, total 0.22 seconds. Tests include source-BruteForce/ILPSolver closed loops, a required skipped-union regression, every small target bitvector, infeasible instances, malformed target rejection, H=1, large atoms, carries, overflowed inactive alternatives, checked layout arithmetic and the canonical example. Formatting passed.
• Prepared local implementation: commit f61809d1, branch contrib/integer-expression-membership-ilp. Full integration, clippy, complete suite, paper and coverage gates remain part of PR preparation and are not claimed complete here.

Counts are assertion/instance-execution counts, not distinct independent random samples. Evidence is prepared locally in research/coauthorship-2026-10-13/verification/algebra_integerexpression*, adversary/adv_integerexpression* and verification/cross_algebra_round1*; these are not yet public links. Proofs, scripts and reports can accompany the verification certificate.

Example

YES source. Let e=((1 ∪ 4)+(3 ∪ 6))+(2 ∪ 5) and K=12. Choices (true,true,false) give 4+6+2=12. Here A=6, S=2, U=3, T=11, H=4, and B=9.

Construction and target. In preorder the activation vector is (1,1,1,0,1,1,0,1,1,1,0). The active leaves, in left-to-right order, are (0,1,0,1,1,0). The complete arithmetic coordinates are:

Concatenating the 11 activation bits, then these 24 prefix bits, then the 18 carry bits gives all 53 target variables. The target has 36 equality rows and 111 nonzeros. At stage 4, bit 2 adds 1+1+0, producing result 0 and outgoing carry 1; at stage 5, bit 1 adds 1+1+0, again producing result 0 and outgoing carry 1. These are precisely the two nonzero carries. The final prefix is 12 and active traversal recovers (true,true,false).

NO source and target. Keep the same tree and set K=7. Each union adds either zero or three to baseline 6, so possible values are exactly {6,9,12,15}. A feasible target's exact prefix identities would likewise make its final total a multiple of three. The imposed final bits for seven contradict that invariant.

Decoder regression. For ((1 ∪ 2) ∪ 3)+(4 ∪ 5) and target 8, the correct output is (true,true,false): the first choice skips the inner left union, the second chooses 5 in the right subtree, and the last bit is unused. Static indices for all union nodes would decode this incorrectly.

BibTeX

@article{Glover1975ImprovedILP,
  author = {Glover, Fred},
  title = {Improved Linear Integer Programming Formulations of Nonlinear Integer Problems},
  journal = {Management Science},
  volume = {22},
  number = {4},
  pages = {455--460},
  year = {1975},
  url = {https://leeds-faculty.colorado.edu/glover/fred%20pubs/69%20-%20Improved%20Linear%20Integer%20Programming%20Formulations%20of%20Nonlinear%20Integer%20Problems%20_%20%20Fred%20Glover.pdf}
}

Attribution and submission status

Responsible human contributor: Thiago Costa (@ThiagoCAltoe). Codex AI agents assisted mathematical discovery, drafting, Rust implementation and independent automated auditing. Human scientific review is pending. No maintainer acceptance, reserved credit or earned coauthorship is claimed; eligibility remains the maintainers' decision.

This proposal is submitted for maintainer review; acceptance and authorship credit remain unconfirmed.