[Model] IntegerExpressionMembership

[isPANN]

Motivation

INTEGER EXPRESSION MEMBERSHIP (P237) from Garey & Johnson, A7 AN18. Given an integer expression built using union (∪) and set addition (+, Minkowski sum) over singleton positive integers, and a target integer K, the problem asks whether K belongs to the set denoted by the expression. NP-complete by reduction from SUBSET SUM (Stockmeyer and Meyer, 1973). Part of a family of problems with varying complexity: the related INEQUIVALENCE problem (do two expressions denote different sets?) is Sigma_2^p-complete, and adding complementation (¬) makes both MEMBERSHIP and INEQUIVALENCE PSPACE-complete. This problem connects formal language theory and arithmetic circuit complexity.

Associated reduction rules:

• As target: R181 (SUBSET SUM to INTEGER EXPRESSION MEMBERSHIP)
• As source: (none known)

Definition

Name: IntegerExpressionMembership

Canonical name: Integer Expression Membership
Reference: Garey & Johnson, Computers and Intractability, A7 AN18

Mathematical definition:

INSTANCE: Integer expression e over the operations ∪ and +, where if n ∈ Z^+, the binary representation of n is an integer expression representing n, and if f and g are integer expressions representing the sets F and G, then f ∪ g is an integer expression representing the set F ∪ G and f + g is an integer expression representing the set {m + n: m ∈ F and n ∈ G}, and a positive integer K.
QUESTION: Is K in the set represented by e?

Variables

• Count: num_union_nodes — the number of Union nodes in the expression tree.
• Per-variable domain: Binary (2 choices per union node: 0 = left branch, 1 = right branch).
• Meaning: Each variable corresponds to one Union node in the expression tree and selects which branch to follow. Given a full assignment of all union choices, the expression collapses to a chain of Sum and Atom nodes that evaluates to a single integer. The problem is satisfiable (Or(true)) iff there exists an assignment of union choices such that the resulting integer equals the target K.
• dims(): vec![2; num_union_nodes]
• Value: Or (feasibility/decision problem)

Schema (data type)

Type name: IntegerExpressionMembership
Variants: none

Field	Type	Description
expression	IntExpr	Integer expression tree over ∪ and + operations
target	u64	Positive integer K to test for membership

Where IntExpr is a recursive type:

• Atom(u64) -- a positive integer literal
• Union(Box<IntExpr>, Box<IntExpr>) -- set union F ∪ G
• Sum(Box<IntExpr>, Box<IntExpr>) -- Minkowski sum {m+n : m ∈ F, n ∈ G}

Size fields (getter methods):

Getter	Type	Description
expression_size	usize	Total number of nodes in the expression tree
num_union_nodes	usize	Number of Union nodes (= number of variables)
num_atoms	usize	Number of Atom leaf nodes
expression_depth	usize	Maximum depth of the expression tree

Complexity

• Best known exact algorithm: Brute-force over all union branch choices. Each Union node is a binary decision; enumerate all 2^d assignments (where d = num_union_nodes), evaluate each to a single integer, and check if any equals K. Time complexity: 2^num_union_nodes (times polynomial overhead per evaluation). No specialized sub-exponential algorithm is known for this problem.
• NP-completeness: Established by Stockmeyer and Meyer (1973) via reduction from SUBSET SUM. [Stockmeyer & Meyer, "Word Problems Requiring Exponential Time," STOC 1973, pp. 1-9; DOI: 10.1145/800125.804029.]
• Related complexity results: The INTEGER EXPRESSION INEQUIVALENCE problem (do two expressions denote different sets?) is Σ₂ᵖ-complete [Stockmeyer & Meyer, 1973; Stockmeyer, TCS 3:1-22, 1976]. Adding complementation (¬) makes both MEMBERSHIP and INEQUIVALENCE PSPACE-complete.

Specialization

• SUBSET SUM is a special case: given set {a_1, ..., a_n} and target B, the expression ({0} ∪ {a_1}) + ({0} ∪ {a_2}) + ... + ({0} ∪ {a_n}) with target B encodes the subset sum question (using a shifted encoding since atoms must be positive).
• INTEGER EXPRESSION INEQUIVALENCE (do two expressions denote different sets?) is Sigma_2^p-complete with ∪ and +.
• With ∪, +, and ¬: both MEMBERSHIP and INEQUIVALENCE become PSPACE-complete.

Extra Remark

Full book text:

INSTANCE: Integer expression e over the operations ∪ and +, where if n ∈ Z^+, the binary representation of n is an integer expression representing n, and if f and g are integer expressions representing the sets F and G, then f ∪ g is an integer expression representing the set F ∪ G and f + g is an integer expression representing the set {m + n: m ∈ F and n ∈ G}, and a positive integer K.
QUESTION: Is K in the set represented by e?

Reference: [Stockmeyer and Meyer, 1973]. Transformation from SUBSET SUM.
Comment: The related INTEGER EXPRESSION INEQUIVALENCE problem, "given two integer expressions e and f, do they represent different sets?" is NP-hard and in fact complete for Σ_2^p in the polynomial hierarchy ([Stockmeyer and Meyer, 1973], [Stockmeyer, 1976a], see also Section 7.2). If the operator "¬" is allowed, with ¬e representing the set of all positive integers not represented by e, then both the membership and inequivalence problems become PSPACE-complete [Stockmeyer and Meyer, 1973].

How to solve

• It can be solved by (existing) bruteforce. (Enumerate all 2^d union-branch assignments where d = num_union_nodes. For each assignment, evaluate the expression to a single integer by collapsing unions to the chosen branch and computing sums. Check if any evaluation equals K.)
• It can be solved by reducing to integer programming. (Not planned. The natural ILP encoding would require exponentially many constraints to capture the recursive set structure.)
• Other: For expressions of bounded depth, dynamic programming on reachable sums at each node. Pseudo-polynomial when atom values are small.

Example Instance

Input:
Expression: e = (2 ∪ 5) + (3 ∪ 7)
Target: K = 10

Analysis:
The set represented by (2 ∪ 5) is {2, 5}.
The set represented by (3 ∪ 7) is {3, 7}.
The Minkowski sum {2, 5} + {3, 7} = {2+3, 2+7, 5+3, 5+7} = {5, 9, 8, 12}.
Set = {5, 8, 9, 12}.

Is K = 10 in {5, 8, 9, 12}? NO.

Another example (YES answer):
Expression: e = (1 ∪ 4) + (3 ∪ 6) + (2 ∪ 5)
Target: K = 12

Set computation:

• {1, 4} + {3, 6} = {4, 7, 7, 10} = {4, 7, 10}
• {4, 7, 10} + {2, 5} = {6, 9, 9, 12, 12, 15} = {6, 9, 12, 15}

Is K = 12 in {6, 9, 12, 15}? YES ✓

Witness path: choose 4 from (1 ∪ 4), choose 6 from (3 ∪ 6), choose 2 from (2 ∪ 5). Sum = 4 + 6 + 2 = 12 = K.

[zazabap]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem but would be an orphan node — neither Subset Sum (source) nor any target exists in the codebase
Non-trivial	✅ Pass	Unique recursive expression tree input structure, distinct from all existing problems
Correctness	⚠️ Warn	References verified (Stockmeyer & Meyer 1973, Stockmeyer 1976) but no concrete best-known algorithm time bound provided
Well-written	❌ Fail	Variables section is vague; Complexity section lacks a concrete time bound; multiple template sections have unverified AI-generated content

Overall: 1 passed, 2 warnings, 1 failed

---

Usefulness

The problem IntegerExpressionMembership does not exist in the codebase — it is a novel addition. However, the issue raises significant usefulness concerns:

• No source reductions exist: The only listed target reduction is from Subset Sum, which is not implemented in this project. There is no SubsetSum model in the codebase.
• No outgoing reductions known: The issue explicitly states "As source: (none known)."
• Orphan node risk: Without at least one implementable reduction rule connecting it to the existing reduction graph, this problem would be an isolated node providing no value to the graph structure.

The motivation mentions connections to "formal language theory and arithmetic circuit complexity" but does not explain how this helps the project's reduction graph.

Non-trivial

Pass. The problem has a genuinely unique input structure — a recursive expression tree (IntExpr) over union and Minkowski sum operations with a target membership query. This is fundamentally different from all existing problems in the codebase:

• Not a graph problem, formula problem, set system, or algebraic/matrix problem
• The recursive tree structure with two distinct operations (union, sum) is novel
• The feasibility constraint (membership in the evaluated set) is structurally distinct from SAT, ILP, etc.

Correctness

References verified:

• Stockmeyer & Meyer, "Word Problems Requiring Exponential Time: Preliminary Report," STOC 1973 — Confirmed real via ACM DL and DBLP. This paper does study membership problems for expressions over sets of integers.
• Stockmeyer, "The Polynomial-Time Hierarchy," Theoretical Computer Science 3:1-22, 1976 — Confirmed real via ScienceDirect.
• Garey & Johnson, Computers and Intractability, A7 AN18 — The book's Appendix A7 covers Algebra and Number Theory problems. The specific AN18 entry cannot be independently verified online but is consistent with the book's structure.

Complexity concern: The issue states the problem is NP-complete but does not provide a concrete worst-case time bound for the best known exact algorithm (e.g., O(2^s) where s is the expression size). The declare_variants! macro requires a concrete complexity string with numeric values. The Complexity section only describes general properties without a usable bound.

Well-written

Failures:

1. Variables section is vague and non-implementable. The section says "Depends on the expression structure" and "the choices made at each '+' node" but never specifies a concrete variable count formula or per-variable domain sizes. For Problem::dims() implementation, the developer needs to know exactly how many variables there are and what domain each has. The current description is a conceptual discussion, not a specification.

2. Complexity section lacks a concrete time bound. The declare_variants! macro requires a complexity string like "2^expression_size". The issue only says "NP-complete" and "the set can have up to 2^s elements" without specifying the actual best-known algorithm's time complexity.

3. Multiple unverified AI-generated warnings. The following sections are flagged with <!-- Unverified: AI-generated -->: Motivation, Rust name, variable description, schema, complexity, specialization, and example. While not automatically disqualifying, this volume of unverified content reduces confidence.

4. How to solve section is incomplete. Only brute-force is checked. The ILP reduction option is unchecked and only sketched ("Encode each union choice as a binary variable..."). For testing reductions, at least one reliable solver path should be fully specified.

5. Schema lacks size getter methods. The overhead system requires getter methods like num_vertices(), num_edges(), etc. The schema defines expression and target fields but doesn't specify what size metrics the problem would expose (e.g., expression_size(), expression_depth(), num_atoms()).

Recommendations

• Define concrete variables: for a decision problem, consider making variables correspond to union choices (binary: left or right branch), giving dims() = vec![2; num_union_nodes].
• Add a concrete complexity bound. Since the set can have up to 2^s elements (where s = expression size), a naive algorithm is O(2^s). If there's a better known bound, cite it with a specific paper.
• Specify size getter methods that the overhead system would use for reduction rules.
• Consider whether this problem should wait until Subset Sum is added, so it can be connected to the reduction graph from day one.

[isPANN]

Issue Quality Check — Model (Re-check)

Previous check: 2026-03-12. Changes: SubsetSum now exists in codebase → Usefulness upgraded from Warn to Pass.

Check	Result	Details
Usefulness	✅ Pass	Novel problem; SubsetSum exists in codebase with planned R181 reduction
Non-trivial	✅ Pass	Unique recursive expression tree input structure, distinct from all 112 existing problem types
Correctness	⚠️ Warn	References verified (Stockmeyer & Meyer 1973, Stockmeyer 1976) but no concrete best-known algorithm time bound found in published literature
Well-written	❌ Fail	Variables section non-implementable; Complexity lacks concrete expression; missing size field getters

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

Pass. The problem IntegerExpressionMembership does not exist in the codebase. Unlike the previous check (2026-03-12), SubsetSum now does exist in the codebase (confirmed via pred show SubsetSum), so the planned R181 (SubsetSum → IntegerExpressionMembership) reduction would directly connect this problem to the existing reduction graph. No outgoing reductions are known, but one incoming edge is sufficient.

Non-trivial

Pass. The recursive expression tree (IntExpr with Atom, Union, Sum) is a genuinely unique input structure. No existing problem in the codebase has a similar recursive-expression-over-set-operations structure. This is clearly a distinct problem, not a variant or repackaging.

Correctness

References verified:

• Stockmeyer & Meyer, STOC 1973, pp. 1-9 — Confirmed via ACM DL (DOI: 10.1145/800125.804029). This is the origin paper for integer expression membership/inequivalence problems. G&J AN18 explicitly cites it with "Transformation from SUBSET SUM."
• Stockmeyer, TCS 3:1-22, 1976 — Confirmed via ScienceDirect. This paper introduces the polynomial hierarchy and is relevant to the Σ₂ᵖ-completeness of the inequivalence problem, not the membership problem directly. The citation is contextually correct (used in the Comment/Extra Remark section about inequivalence).
• G&J A7 AN18 — Confirmed match for "Integer Expression Membership" with the exact definition and reference chain.

Warn: No concrete time bound. No published literature provides a refined exponential bound for this specific problem (unlike MIS at 1.1996ⁿ or SubsetSum at 2^{n/2}). The naive brute-force is O(2^s) where s = expression size (number of nodes), since the represented set can have up to 2^s elements. A pseudo-polynomial DP exists when atom values are small. The declare_variants! macro requires a concrete complexity string — the issue must provide one.

Well-written

Failures:

1. Variables section is non-implementable. The section says "Depends on the expression structure" and discusses "choices at each '+' node" without specifying a concrete variable count or per-variable domain. For Problem::dims(), the developer needs an exact formula. Suggested fix: Variables correspond to union choices in the expression tree — each union node is a binary variable (left=0, right=1). So dims() = vec![2; num_union_nodes]. The total variable count is the number of union nodes in the expression.

2. Complexity section lacks a concrete time bound expression. The declare_variants! macro needs something like "2^expression_size" or "2^num_union_nodes". The section only says "NP-complete" and discusses general properties. Suggested fix: Use "2^num_union_nodes" (brute-force over all union branch choices).

3. Missing size field getter specifications. The Schema defines expression and target fields but doesn't specify what size metrics the problem exposes. Suggested fix: Add a size fields table with getters like expression_size() (total nodes in expression tree), num_union_nodes() (number of union choice points), num_atoms() (number of leaf/atom nodes), target() (the value K).

4. How to solve section is incomplete. ILP is unchecked but partially sketched. If ILP is not planned, that's fine, but the sketch should be removed or the box should be explicitly marked as not applicable.

Examples validated correctly (verified via Python script):

• Example 1: (2 ∪ 5) + (3 ∪ 7), K=10 → set = {5, 8, 9, 12} → NO ✓
• Example 2: (1 ∪ 4) + (3 ∪ 6) + (2 ∪ 5), K=12 → set = {6, 9, 12, 15} → YES ✓ (witness: 4+6+2=12)

Example 2 quality: 3 union choice points → 8 total paths → 4 distinct sums → 3 paths produce K=12, 5 do not. Adequate for round-trip testing.

Recommendations

• Define variables as union choices: dims() = vec![2; num_union_nodes]. A configuration is a binary vector indicating left/right at each union; evaluate by selecting the chosen branch at each union, then computing the sum. Membership iff any configuration yields K.
• Add a concrete complexity string: "2^num_union_nodes" (exhaustive search over union choices).
• Specify size getters: expression_size, num_union_nodes, num_atoms, expression_depth.
• Consider adding a slightly more complex example with nested expressions (not just a flat chain of sums over unions) to exercise the recursive structure more thoroughly.

[isPANN]

Fix-issue changelog

• Variables section: Rewrote with concrete definition — count = num_union_nodes, domain = binary (left/right branch), dims() = vec![2; num_union_nodes], Value = Or
• Complexity section: Added concrete bound 2^num_union_nodes (brute-force); restructured to separate NP-completeness proof from algorithm bound
• Schema section: Added Size fields table with 4 getters: expression_size, num_union_nodes, num_atoms, expression_depth (consistent with rule [Rule] SUBSET SUM to INTEGER EXPRESSION MEMBERSHIP #569 overhead references)
• How to solve: Rewrote brute-force description to match variable formulation; struck through ILP option with explanation

Applied by /fix-issue.