[Model] SimultaneousIncongruences

[isPANN]

Motivation

SIMULTANEOUS INCONGRUENCES (P221) from Garey & Johnson, A7 AN2. An NP-complete number-theoretic problem: given a collection of forbidden residue classes {(aᵢ, bᵢ)}, determine whether there exists an integer x that avoids all of them (x ≢ aᵢ mod bᵢ for each i). Related to covering systems in number theory. NP-complete by Stockmeyer and Meyer (1973) via reduction from 3SAT. Despite the simplicity of the question (find an integer outside a union of arithmetic progressions), the interaction of different moduli makes the problem intractable.

Associated reduction rules:

• R165: 3SAT → SimultaneousIncongruences (this model is the target)

Definition

Name: SimultaneousIncongruences
Reference: Garey & Johnson, Computers and Intractability, A7 AN2

Mathematical definition:

INSTANCE: Collection {(a₁, b₁), …, (aₙ, bₙ)} of ordered pairs of positive integers, with aᵢ ≤ bᵢ for 1 ≤ i ≤ n.
QUESTION: Is there an integer x such that x ≢ aᵢ (mod bᵢ) for all 1 ≤ i ≤ n?

This is a satisfaction (feasibility) problem: Value = Or.

Variables

• Count: 1 (the unknown integer x)
• Per-variable domain: lcm(b₁, …, bₙ) — by periodicity, it suffices to search one period of the combined modular system. Values 0, 1, …, lcm − 1.
• Meaning: The single variable represents the candidate integer x. The evaluate function checks whether x mod bᵢ ≠ aᵢ for all i.

dims() returns [lcm(b₁, …, bₙ)].

Note: The lcm can be exponential in the input bit-length (this is the source of NP-completeness). For small moduli the search is fast; for large moduli, brute-force may be impractical. The dims() contract is satisfied (lcm fits in usize for representable instances).

Schema (data type)

Type name: SimultaneousIncongruences
Variants: none

Field	Type	Description	Getter
pairs	Vec<(u64, u64)>	Collection of (aᵢ, bᵢ) pairs; x ≢ aᵢ (mod bᵢ). Constraint: 1 ≤ aᵢ ≤ bᵢ.	num_pairs() → self.pairs.len()

Problem type: Satisfaction (feasibility)
Value type: Or

Complexity

• Decision complexity: NP-complete (Stockmeyer & Meyer, 1973; transformation from 3SAT).
• Best known exact algorithm: Brute-force search over x ∈ {0, …, lcm(b₁,…,bₙ) − 1}, checking all n conditions. Time O(lcm · n), pseudo-polynomial.
• Complexity string for declare_variants!: "num_pairs" (per-candidate check is O(n); the search space lcm is data-dependent, not expressible as a simple getter)
• Special cases: For fixed moduli (all bᵢ bounded by a constant), polynomial. For moduli that form a covering system, the answer is always NO.
• References:
  • [Stockmeyer & Meyer, 1973] L. J. Stockmeyer and A. R. Meyer, "Word problems requiring exponential time", STOC 1973, pp. 1-9.

Extra Remark

Full book text:

INSTANCE: Collection {(a_1,b_1), . . . , (a_n,b_n)} of ordered pairs of positive integers, with a_i <= b_i for 1 <= i <= n.
QUESTION: Is there an integer x such that, for 1 <= i <= n, x ≢ a_i (mod b_i)?

Reference: [Stockmeyer and Meyer, 1973]. Transformation from 3SAT.

How to solve

• It can be solved by (existing) bruteforce. Enumerate x from 0 to lcm(b₁,…,bₙ) − 1; check all n incongruence conditions. For small lcm this is fast.
• It can be solved by reducing to integer programming. (The incongruence constraints x mod bᵢ ≠ aᵢ are not directly expressible as linear equalities/inequalities.)
• Other: Sieving methods for special structure; polynomial for bounded moduli.

Example Instance

Positive example (YES):
n = 4 pairs: (2, 2), (1, 3), (2, 5), (3, 7)

Meaning: x ≢ 2 (mod 2), x ≢ 1 (mod 3), x ≢ 2 (mod 5), x ≢ 3 (mod 7).

lcm(2, 3, 5, 7) = 210. Search space: {0, …, 209}.

Solution search (first few candidates):

x	x mod 2 ≠ 0?	x mod 3 ≠ 1?	x mod 5 ≠ 2?	x mod 7 ≠ 3?	Result
0	0 = 0 ✗	—	—	—	Fail
1	1 ≠ 0 ✓	1 = 1 ✗	—	—	Fail
2	0 = 0 ✗	—	—	—	Fail
3	1 ≠ 0 ✓	0 ≠ 1 ✓	3 ≠ 2 ✓	3 = 3 ✗	Fail
4	0 = 0 ✗	—	—	—	Fail
5	1 ≠ 0 ✓	2 ≠ 1 ✓	0 ≠ 2 ✓	5 ≠ 3 ✓	Pass

Answer: Or(true). x = 5 satisfies all incongruences.

Verification: 5 mod 2 = 1 ≠ 0 ✓; 5 mod 3 = 2 ≠ 1 ✓; 5 mod 5 = 0 ≠ 2 ✓; 5 mod 7 = 5 ≠ 3 ✓.

Out of 210 candidates, 48 are solutions and 162 are non-solutions — good coverage for round-trip testing.

Negative example (NO — covering system):
n = 2 pairs: (1, 2), (2, 2)

• (1, 2): x ≢ 1 (mod 2) → x must be even
• (2, 2): x ≢ 0 (mod 2) → x must be odd

These two conditions are contradictory — no integer x can be both even and odd. Answer: Or(false).

Expected outcome: Or(true) for the primary example.

Reduction Rule Crossref

• R165: Satisfiability (3SAT) → SimultaneousIncongruences

[zazabap]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but only one planned reduction (3SAT target); no source reductions identified
Non-trivial	✅ Pass	Genuinely distinct: modular arithmetic constraints differ from all existing models
Correctness	✅ Pass	Stockmeyer & Meyer (1973) reference verified; GJ A7 AN2 classification consistent
Well-written	❌ Fail	Missing complexity string for declare_variants!; exponential variable domain makes dims() problematic; no size fields defined

Overall: 1 passed, 1 warning, 1 failed (Correctness pass, Well-written fail)

---

Usefulness

The problem does not exist in the codebase and is a genuinely novel addition from Garey & Johnson's appendix (A7 AN2). The motivation is substantive — it explains the number-theoretic significance and the source of NP-completeness (interaction of different moduli).

However, the issue lists no source reductions (only a target reduction from 3SAT via R165). A problem with only one inbound reduction and no outbound reductions has limited graph connectivity value. This is a warning, not a failure — the problem is still useful as a target.

Non-trivial

This is clearly a distinct problem. The feasibility constraint (avoiding forbidden residue classes modulo different bases) is fundamentally different from all existing models:

• Not a graph problem
• Not a boolean formula
• Not a set system
• Not a matrix/linear algebra problem

The modular arithmetic structure is genuinely new to the codebase.

Correctness

• Stockmeyer & Meyer (1973) — Verified. The paper "Word Problems Requiring Exponential Time (Preliminary Report)" was presented at STOC 1973. The NP-completeness of Simultaneous Incongruences via reduction from 3SAT is an established result attributed to them in the Garey & Johnson compendium.
• Garey & Johnson A7 AN2 — Consistent with the standard GJ problem numbering (Algebra and Number Theory, problem 2).
• Complexity description — The pseudo-polynomial brute-force analysis is correct: searching over {0, ..., lcm(b_1,...,b_n)-1} with n checks per candidate gives O(lcm * n), which is pseudo-polynomial since the LCM can be exponential in the input size (measured in bits).

Well-written

Several issues need to be addressed:

1. Missing declare_variants! complexity string. The Complexity section describes the brute-force approach qualitatively but does not provide a concrete worst-case complexity expression (e.g., "2^num_pairs" or similar) needed for the declare_variants! macro. Since the brute-force is pseudo-polynomial with an exponential LCM, the issue should specify what the best known exact algorithm is and its time bound in terms of the problem's getter methods.

2. Exponential variable domain is problematic for dims(). The Problem trait requires fn dims(&self) -> Vec<usize> returning per-variable domain sizes. With a single variable x in {0, ..., lcm-1}, dims() would return vec![lcm] where lcm can be astronomically large (or overflow usize). This is a fundamental design issue that needs to be addressed in the schema. Consider:

   • Using a binary encoding of x (n bits, where n = ceil(log2(lcm))), giving dims() = vec![2; n]
   • Or capping the domain and documenting the limitation

3. No size fields / getter methods defined. The Schema section does not specify what getter methods the type should expose (e.g., num_pairs(), max_modulus(), lcm_moduli()). These are needed for overhead expressions in future reduction rules and for declare_variants! complexity strings.

4. Problem type not explicitly stated. The issue should clearly state this is a satisfaction problem (Metric = bool, implements SatisfactionProblem), not an optimization problem.

5. Missing "How to solve" detail. The brute-force checkbox is checked but the description is vague about how to handle the potentially enormous search space in practice. If using binary encoding, the brute-force would enumerate all 2^n bit strings.

Recommendations

• Add a concrete complexity string (e.g., based on the number of pairs and the product of moduli)
• Define size fields: num_pairs, and possibly max_modulus or log_lcm
• Clarify the variable encoding: recommend binary encoding of x to fit the dims() contract
• Explicitly state SatisfactionProblem trait implementation

[isPANN]

Issue Quality Check — Model

Re-check (previous check from 2026-03-12: 1 passed, 1 warning, 1 failed. Current re-check below).

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem not in codebase; only one inbound reduction (3SAT target), no outbound reductions
Non-trivial	✅ Pass	Modular arithmetic feasibility constraints are genuinely distinct from all 116 existing problem types
Correctness	✅ Pass	Stockmeyer & Meyer (1973) verified; GJ A7 AN2 classification consistent; example verified numerically
Well-written	❌ Fail	Missing complexity string, no size fields, exponential dims() domain unaddressed, problem type unstated

Overall: 1 passed, 1 warning, 1 failed

---

Usefulness

SimultaneousIncongruences does not exist in the codebase (pred show SimultaneousIncongruences fails). The problem is a genuine addition from Garey & Johnson's appendix (A7, Algebra and Number Theory). The motivation explains the number-theoretic significance well.

However, the issue lists only one inbound reduction (R165: 3SAT -> Simultaneous Incongruences) and no outbound reductions. A problem with only one edge has limited graph connectivity value. Warning (not failure) — single-edge problems are still useful as targets.

Non-trivial

The feasibility constraint (find an integer avoiding all forbidden residue classes modulo different bases) is fundamentally different from all 116 existing problem types:

• Not a graph problem, boolean formula, set system, or matrix/linear algebra problem
• The modular arithmetic structure with mixed moduli is genuinely novel in the codebase

Pass.

Correctness

Reference verification:

• Stockmeyer & Meyer (1973) — Verified. "Word Problems Requiring Exponential Time: Preliminary Report" appeared at STOC 1973 (confirmed via DBLP and ACM DL). The NP-completeness of Simultaneous Incongruences via reduction from 3SAT is attributed to this work in the Garey & Johnson compendium.
• Garey & Johnson A7 AN2 — Consistent with the book's Algebra and Number Theory appendix section structure.

Complexity analysis: The pseudo-polynomial brute-force description is correct: searching {0, ..., lcm(b_1,...,b_n)-1} with n checks per candidate gives O(lcm * n), which is pseudo-polynomial since the LCM can be exponential in the input size (measured in bits).

Example verification (Python brute-force):

• Example 1: pairs = [(0,2), (1,3), (2,5), (3,7)], LCM = 210, found 48 satisfying values out of 210 candidates. Claimed solution x=5 is correct (verified: 5 mod 2=1≠0, 5 mod 3=2≠1, 5 mod 5=0≠2, 5 mod 7=5≠3).
• Example 2 (negative): pairs = [(0,2), (1,2)], LCM = 2, 0 satisfying values — correctly unsatisfiable.
• Round-trip quality: 48 satisfying + 162 non-satisfying configs — good mix for testing.

Pass.

Well-written

The following issues from the previous review (2026-03-12) remain unaddressed:

1. Missing declare_variants! complexity string. The Complexity section describes the brute-force qualitatively but does not provide a concrete worst-case expression in terms of getter methods (e.g., something based on num_pairs or product of moduli). This is required for the declare_variants! macro.

2. Exponential variable domain problematic for dims(). The Problem trait requires fn dims(&self) -> Vec<usize> returning per-variable domain sizes. With a single variable x in {0, ..., lcm-1}, dims() would return vec![lcm] where lcm can overflow usize. The issue must propose a concrete encoding strategy:

   • Binary encoding of x (n = ceil(log2(lcm)) bits, giving dims() = vec![2; n])
   • Or capping the domain with documented limitations

3. No size fields / getter methods defined. The Schema section does not specify getter methods (e.g., num_pairs(), max_modulus(), lcm_moduli()). These are needed for overhead expressions in future reduction rules and for declare_variants! complexity strings.

4. Problem type not explicitly stated. The issue should state this is a satisfaction problem (Value type Or), not an optimization problem.

5. Missing "How to solve" detail. The brute-force checkbox is checked but does not address the exponential search space in practice. If binary encoding is used, the brute-force would enumerate 2^n bit strings where n = ceil(log2(lcm)).

Fail — items 1-4 are required for implementation.

Recommendations

• Add a concrete complexity string (e.g., "2^log_lcm * num_pairs" or similar, using getter method names)
• Define size fields: num_pairs, and log_lcm or max_modulus
• Clarify the variable encoding: recommend binary encoding of x to fit the dims() contract
• Explicitly state Value = Or (satisfaction problem)
• Consider whether the negative example (which is trivially unsatisfiable) should be the canonical example, or whether the positive 4-pair example is sufficient — both are good to include

[isPANN]

Issue Quality Check — Model (Re-check)

Re-check (previous checks from 2026-03-12 and 2026-03-29 both found: 1 pass, 1 warning, 1 fail. This re-check finds the same overall verdict with one new correctness finding.)

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem not in codebase; only one inbound reduction (3SAT), no outbound reductions
Non-trivial	✅ Pass	Modular arithmetic feasibility constraints are genuinely distinct from all existing problem types
Correctness	⚠️ Warn	References verified, but example violates the stated GJ definition (uses a_i = 0, which is not a positive integer)
Well-written	❌ Fail	Missing complexity string, no size fields, exponential dims() domain unaddressed, problem type unstated

Overall: 1 passed, 2 warnings, 1 failed

Change from previous checks: Previously Correctness was Pass — now downgraded to Warn due to newly discovered example constraint violation (see below). All other verdicts unchanged.

---

Usefulness

SimultaneousIncongruences does not exist in the codebase (pred show SimultaneousIncongruences returns "Unknown problem"). The problem is a genuine addition from Garey & Johnson's appendix (A7, Algebra and Number Theory, AN2). The motivation explains the number-theoretic significance well.

However, the issue lists only one inbound reduction (R165: 3SAT -> Simultaneous Incongruences) and no outbound reductions. A problem with only one edge has limited graph connectivity value. Warning — single-edge problems are still useful as targets.

Non-trivial

The feasibility constraint (find an integer avoiding all forbidden residue classes modulo different bases) is fundamentally different from all existing problem types. Not a graph problem, boolean formula, set system, or matrix/linear algebra problem. The modular arithmetic structure with mixed moduli is genuinely novel.

Pass.

Correctness

Reference verification:

• Stockmeyer & Meyer (1973) — Verified. "Word Problems Requiring Exponential Time: Preliminary Report" appeared at STOC 1973. Already in the project bibliography as stockmeyer1973 (DOI: 10.1145/800125.804029). The NP-completeness of Simultaneous Incongruences via reduction from 3SAT is attributed to this work in the Garey & Johnson compendium.
• Garey & Johnson A7 AN2 — Consistent with the book's Algebra and Number Theory appendix.

Complexity analysis: The pseudo-polynomial brute-force description is correct: searching {0, ..., lcm(b_1,...,b_n)-1} with n checks per candidate gives O(lcm * n), which is pseudo-polynomial since the LCM can be exponential in the input size.

Example verification (Python brute-force):

• Example 1: pairs = [(0,2), (1,3), (2,5), (3,7)], LCM = 210, found 48 satisfying values out of 210 candidates. Claimed solution x=5 is numerically correct.
• Example 2 (negative): pairs = [(0,2), (1,2)], LCM = 2, 0 satisfying values — correctly unsatisfiable.
• Round-trip quality: 48 satisfying + 162 non-satisfying configs — good mix for testing.

NEW FINDING — Example constraint violation: The GJ definition specifies "ordered pairs of positive integers, with a_i <= b_i for 1 <= i <= n." However, both examples use a_i = 0, which is not a positive integer. Specifically:

• Example 1 uses (0, 2) — a_1 = 0 is not positive
• Example 2 uses (0, 2) — same issue

Mathematically this is fixable: x ≡ 0 (mod 2) is equivalent to x ≡ 2 (mod 2), so (0, 2) can be replaced with (2, 2) to satisfy the GJ constraint. But the issue body should either (a) fix the examples to use positive integers per GJ, or (b) explicitly note that the implementation relaxes the constraint to non-negative integers (a_i in {0, ..., b_i-1}) for convenience. This is a Warning rather than a Fail because the mathematical content is correct and the fix is straightforward.

Well-written

The following issues from the previous two reviews (2026-03-12 and 2026-03-29) remain unaddressed:

1. Missing declare_variants! complexity string. The Complexity section describes the brute-force qualitatively but does not provide a concrete worst-case expression in terms of getter methods. This is required for the declare_variants! macro. Since the LCM can be exponential, a concrete expression is needed (e.g., based on num_pairs or product of moduli).

2. Exponential variable domain problematic for dims(). The Problem trait requires fn dims(&self) -> Vec<usize> returning per-variable domain sizes. With a single variable x in {0, ..., lcm-1}, dims() would return vec![lcm] where lcm can overflow usize. The issue must propose a concrete encoding strategy:

   • Binary encoding of x (n = ceil(log2(lcm)) bits, giving dims() = vec![2; n])
   • Or capping the domain with documented limitations

3. No size fields / getter methods defined. The Schema section does not specify getter methods (e.g., num_pairs(), max_modulus(), lcm_moduli()). These are needed for overhead expressions and declare_variants! complexity strings.

4. Problem type not explicitly stated. The issue should state this is a satisfaction problem (Value type Or), not an optimization problem.

5. Missing "How to solve" detail. The brute-force checkbox is checked but does not address the exponential search space. If binary encoding is used, the brute-force would enumerate 2^n bit strings where n = ceil(log2(lcm)).

Fail — items 1-4 are required for implementation.

Recommendations

• Fix examples to use positive integers per GJ definition (replace (0, 2) with (2, 2)) or explicitly document the relaxation
• Add a concrete complexity string using getter method names
• Define size fields: num_pairs, and log_lcm or max_modulus
• Clarify the variable encoding to fit the dims() contract
• Explicitly state Value = Or (satisfaction problem)

[isPANN]

Fix-issue changelog

• Fixed aᵢ = 0 violations: replaced (0, 2) with (2, 2) since 0 ≡ 2 (mod 2), satisfying GJ's aᵢ ≥ 1 constraint
• Fixed negative example: (1, 2), (2, 2) is a valid covering system with aᵢ ≥ 1
• Added explicit problem type: satisfaction, Value = Or
• Added dims() mapping: [lcm(b₁,…,bₙ)] with note about exponential lcm
• Added getter method (num_pairs())
• Added complexity string num_pairs for declare_variants!
• Added full solution/non-solution counts (48/210) for round-trip testing
• Noted ILP is not directly applicable (incongruence ≠ linear constraint)
• Removed "Unverified" markers from verified content

Applied by /fix-issue.