[Model] QuadraticCongruences

[isPANN]

Motivation

QUADRATIC CONGRUENCES (P220) from Garey & Johnson, A7 AN1. A classical NP-complete problem in number theory: given positive integers a, b, c, determine if there exists a positive integer x < c with x² ≡ a (mod b). The problem is NP-complete due to the upper bound constraint x < c; without this bound, the problem is polynomial-time solvable given the factorization of b. This is a cornerstone result by Manders and Adleman (1978) connecting computational complexity to quadratic residuosity.

Associated reduction rules:

• R164: 3SAT → QuadraticCongruences (this model is the target)

Definition

Name: QuadraticCongruences
Reference: Garey & Johnson, Computers and Intractability, A7 AN1

Mathematical definition:

INSTANCE: Positive integers a, b, and c.
QUESTION: Is there a positive integer x with 1 ≤ x < c such that x² ≡ a (mod b)?

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

Variables

• Count: 1 (the unknown x)
• Per-variable domain: c − 1 (values 1, 2, …, c − 1)
• Meaning: The single variable represents the candidate integer x. The evaluate function checks whether x² mod b = a.

dims() returns [c - 1].

Note: When c is large (exponential in the input bit-length), the brute-force search space is correspondingly large. The dims() contract is satisfied (c − 1 fits in usize for representable instances), but brute-force may be impractical for large c. This is expected for an NP-complete problem — the NP-completeness arises precisely from the exponential range of c relative to input size.

Schema (data type)

Type name: QuadraticCongruences
Variants: none (operates on three positive integers)

Field	Type	Description	Getter
a	u64	Target residue (x² ≡ a mod b)	a()
b	u64	Modulus	b()
c	u64	Upper bound on x (exclusive); 1 ≤ x < c	c()

Problem type: Satisfaction (feasibility)
Value type: Or

Complexity

• Decision complexity: NP-complete (Manders & Adleman, 1978; transformation from 3SAT). Remains NP-complete even if the prime factorization of b and solutions modulo all prime powers are given.
• Best known exact algorithm: Brute-force enumeration of x ∈ {1, …, c−1}, checking x² mod b = a. Time O(c · polylog(b)), which is pseudo-polynomial.
• Complexity string for declare_variants!: "c" (brute-force iterates over all x < c)
• Special cases:
  • c = ∞ (no upper bound) with factorization of b given: polynomial (CRT + Hensel lifting)
  • b prime, assuming ERH: polynomial (Tonelli-Shanks algorithm)
• References:
  • [Manders & Adleman, 1978] K. Manders and L. Adleman, "NP-complete decision problems for binary quadratics", JCSS 16(2), pp. 168-184, 1978.

Extra Remark

Full book text:

INSTANCE: Positive integers a, b, and c.
QUESTION: Is there a positive integer x < c such that x^2 ≡ a (mod b)?

Reference: [Manders and Adleman, 1978]. Transformation from 3SAT.
Comment: Remains NP-complete even if the instance includes a prime factorization of b and solutions to the congruence modulo all prime powers occurring in the factorization. Solvable in polynomial time if c = ∞ (i.e., there is no upper bound on x) and the prime factorization of b is given. Assuming the Extended Riemann Hypothesis, the problem is solvable in polynomial time when b is prime. The general problem is trivially solvable in pseudo-polynomial time.

How to solve

• It can be solved by (existing) bruteforce. Enumerate x from 1 to c−1; check if x² mod b = a. For small c this is fast; for large c it may be impractical.
• It can be solved by reducing to integer programming. (The constraint x² ≡ a (mod b) is quadratic, not directly expressible as a linear constraint.)
• Other: For special cases (b prime, c = ∞), polynomial-time algorithms exist (Tonelli-Shanks, CRT + Hensel lifting).

Example Instance

Positive example (YES):
a = 4, b = 15, c = 10

Question: Is there x ∈ {1, 2, …, 9} with x² ≡ 4 (mod 15)?

Solution search:

x	x²	x² mod 15	Match?
1	1	1	No
2	4	4	Yes ✓
3	9	9	No
4	16	1	No
5	25	10	No
6	36	6	No
7	49	4	Yes ✓
8	64	4	Yes ✓
9	81	6	No

Answer: Or(true). Three solutions exist: x = 2, x = 7, x = 8. Six non-solutions provide meaningful negative coverage.

Verification: 2² = 4 ≡ 4 (mod 15) ✓; 7² = 49 = 3·15 + 4 ✓; 8² = 64 = 4·15 + 4 ✓.

Negative example (NO):
a = 3, b = 7, c = 7

Quadratic residues mod 7: {1² ≡ 1, 2² ≡ 4, 3² ≡ 2, 4² ≡ 2, 5² ≡ 4, 6² ≡ 1} = {1, 2, 4}.
Since 3 ∉ {1, 2, 4}, no x satisfies x² ≡ 3 (mod 7). Answer: Or(false).

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

Reduction Rule Crossref

• R164: Satisfiability (3SAT) → QuadraticCongruences

[zazabap]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but leaf node with only one incoming rule and no outgoing rules
Non-trivial	✅ Pass	Genuinely distinct; number-theoretic problem unlike anything in the codebase
Correctness	✅ Pass	Manders & Adleman (1978) verified; GJ A7 AN1 definition matches
Well-written	❌ Fail	Variable domain can be exponential, making brute-force impractical; missing complexity string

Overall: 2 passed, 1 failed, 1 warning

---

Usefulness

The problem does not exist in the codebase and is genuinely novel — it is the first number-theoretic problem proposed. However, it would be a leaf node in the reduction graph: only one incoming rule (3SAT → QuadraticCongruences, from Manders & Adleman) and no known outgoing rules. Without outgoing reductions, the problem cannot serve as a source for solving other problems. This limits its immediate utility in the reduction framework. Warning, not failure, since the incoming rule from 3SAT is valuable.

Non-trivial

The problem is fundamentally different from all existing problems. It involves modular arithmetic and quadratic residuosity — a number-theoretic domain not represented in the codebase. No existing problem can be trivially renamed or restricted to produce this. Clear pass.

Correctness

• ✅ Garey & Johnson (1979) — The problem definition matches GJ A7 AN1 verbatim.
• ✅ Manders & Adleman (1978) — Verified: "NP-complete decision problems for binary quadratics," Journal of Computer and System Sciences 16, pp. 168–184. The paper proves NP-completeness of quadratic congruences via reduction from 3SAT. Originally appeared at STOC 1976.
• ✅ The complexity discussion is accurate: the problem is trivially solvable in pseudo-polynomial time, polynomial when b is prime under ERH (Tonelli-Shanks), and polynomial when c = infinity with factorization of b given.
• ✅ The example is correct: 3^2 = 9 ≡ 2 (mod 7). The negative example correctly identifies 3 as a quadratic non-residue mod 7.

Well-written

Critical issue — exponential variable domain:
The variable x ranges over {1, ..., c-1}. Since the input is the binary encoding of (a, b, c), the value c can be exponential in the input bit-length (up to 2^n where n is the number of bits). This means:

• dims() would return vec![c - 1], which could be 2^64 or larger
• The brute-force solver iterates over all configurations — it would be completely impractical
• The u64 type in the schema limits c to 2^64, but even 2^32 is too large for brute-force

This is a fundamental impedance mismatch with the framework's Problem trait, which assumes configuration spaces are enumerable. The issue should address this explicitly and propose a mitigation (e.g., restrict to small instances for testing, or note that brute-force is pseudo-polynomial).

Other issues:

1. No concrete complexity string for declare_variants!: The brute-force bound is O(c * polylog(b)), but c is not a structural parameter accessible via a getter — it is the search bound. The issue needs to specify what declare_variants! complexity string to use. Perhaps "c" or express in terms of input bit-length.
2. ILP reduction unchecked: The issue does not explore ILP formulation. While modular arithmetic is harder to express in ILP, this should be explicitly marked as infeasible or investigated.
3. Schema uses u64: For consistency with the problem (positive integers that could be large), consider whether u64 suffices or if big integers are needed. For practical implementation with brute-force, u64 is fine but should be documented as a limitation.
4. Missing getter method names: The issue should specify a(), b(), modulus(), upper_bound(), etc. Note that b() as a method name may conflict with Rust conventions.
5. Example is minimal but correct. The positive instance (a=2, b=7, c=6) and negative instance (a=3, b=7, c=7) are good — small enough to verify by hand and demonstrate both YES and NO cases.

Recommendations

• Address the exponential domain issue explicitly: acknowledge that brute-force is pseudo-polynomial and only practical for small c. Consider adding a num_bits() getter that returns the bit-length of c, and express complexity in terms of that.
• Provide a concrete declare_variants! string (e.g., "c" as pseudo-polynomial bound, or "2^num_bits" for true worst-case).
• Rename schema fields to avoid single-letter names that could conflict: target_residue, modulus, upper_bound.
• Explicitly state that ILP reduction is not feasible for this problem (modular arithmetic is not naturally linearizable).

[isPANN]

Issue Quality Check — Model

Re-check (previous check from 2026-03-12). Previously: 2 passed, 1 failed, 1 warning.

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but leaf node — only one incoming rule (3SAT → QC), no outgoing rules
Non-trivial	✅ Pass	Genuinely distinct number-theoretic problem; no existing codebase equivalent
Correctness	✅ Pass	Manders & Adleman (1978) verified; GJ A7 AN1 definition matches; examples numerically correct
Well-written	❌ Fail	Exponential variable domain incompatible with brute-force dims(); missing complexity string; incomplete worked example

Overall: 2 passed, 1 failed, 1 warning

---

Usefulness

The problem does not exist in the codebase (pred show QuadraticCongruences fails). It is the first number-theoretic problem proposed and would be a genuinely novel node. However, it remains a leaf node: the only known reduction is 3SAT → QuadraticCongruences (Manders & Adleman 1978). No outgoing rules are known, limiting its utility as a reduction source. Warning, not failure, since the incoming NP-completeness proof from 3SAT is historically significant.

Non-trivial

The problem involves modular arithmetic and quadratic residuosity — a domain not represented by any existing problem in the codebase. It has genuinely different feasibility constraints (x^2 ≡ a mod b with x < c) from all 116 existing problem types. Clear pass.

Correctness

• ✅ Manders & Adleman (1978) — Verified via Semantic Scholar and ScienceDirect: "NP-Complete Decision Problems for Binary Quadratics," Journal of Computer and System Sciences 16, pp. 168–184. The paper proves NP-completeness via reduction from SAT (originally presented at STOC 1976). The issue's citation is correct.
• ✅ Garey & Johnson (1979) — The problem definition matches GJ A7 AN1. The "Extra Remark" section correctly quotes the GJ commentary about polynomial-time solvability when c = ∞ with factorization, and under ERH when b is prime.
• ✅ Examples numerically verified via Python script:
  • Positive: a=2, b=7, c=6 → x=3 satisfies 3²=9≡2 (mod 7). Also x=4 satisfies 4²=16≡2 (mod 7).
  • Negative: a=3, b=7, c=7 → QR mod 7 = {1, 2, 4}, so 3 is a non-residue. No solution exists.

Well-written

Failures:

1. Exponential variable domain breaks dims() contract. The variable x ranges over {1, ..., c−1}. Since input is binary-encoded, c can be exponential in the bit-length (up to 2^64 for u64). The Problem trait's dims() method returns Vec<usize>, which the brute-force solver enumerates exhaustively. For large c, dims() → vec![c - 1] would create an astronomically large search space. The issue must address this impedance mismatch — e.g., by explicitly restricting to small c for testing, or by documenting that brute-force is pseudo-polynomial and only practical for small instances.

2. No concrete declare_variants! complexity string. The complexity section discusses O(c · polylog(b)) but does not provide a concrete expression in terms of getter-accessible parameters (e.g., "c" or "2^num_bits"). The declare_variants! macro requires a compile-time string referencing getter methods.

3. Incomplete worked example. The "Solution search" stops at x=3 without checking x=4 and x=5. Python verification shows x=4 is also a solution (4² = 16 ≡ 2 mod 7). A fully worked example must enumerate all candidates or explicitly state "we stop at the first solution found."

4. Missing getter method names in Schema. The overhead system and declare_variants! require getter methods. The issue should specify what getters the struct provides (e.g., a(), modulus(), upper_bound()). Note: b() as a method name is problematic in Rust.

Warnings (non-blocking):

• The issue does not explore ILP formulation feasibility. Modular arithmetic is not naturally linearizable, so the unchecked ILP box should be explicitly marked infeasible with a brief note.
• Schema uses single-letter field names (a, b, c) which may cause naming conflicts. Consider target_residue, modulus, upper_bound.

Recommendations

• Address the exponential domain issue by adding a paragraph to the Schema section acknowledging the pseudo-polynomial nature and restricting practical brute-force to small c (e.g., c ≤ 10^6).
• Provide a concrete declare_variants! complexity string. Since the brute-force bound is O(c), and c is representable as an input field, consider "upper_bound" (pseudo-polynomial) or express in terms of input bit-length.
• Complete the worked example by showing all 5 evaluations (x=1 through x=5) or noting that the search can stop early.
• Rename schema fields to avoid single-letter conflicts: target_residue, modulus, upper_bound.

[isPANN]

Issue Quality Check — Model

Re-check (previous check from 2026-03-12). Previously: 2 passed, 1 failed, 1 warning.

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but leaf node — only one incoming rule (3SAT → QC), no outgoing rules
Non-trivial	✅ Pass	Genuinely distinct number-theoretic problem; no existing codebase equivalent
Correctness	✅ Pass	Manders & Adleman (1978) verified; GJ A7 AN1 definition matches; examples numerically correct
Well-written	❌ Fail	Exponential variable domain incompatible with brute-force dims(); missing complexity string; incomplete worked example

Overall: 2 passed, 1 failed, 1 warning

---

Usefulness

The problem does not exist in the codebase (pred show QuadraticCongruences fails). It is the first number-theoretic problem proposed and would be a genuinely novel node. However, it remains a leaf node: the only known reduction is 3SAT → QuadraticCongruences (Manders & Adleman 1978). No outgoing rules are known, limiting its utility as a reduction source. Warning, not failure, since the incoming NP-completeness proof from 3SAT is historically significant.

Non-trivial

The problem involves modular arithmetic and quadratic residuosity — a domain not represented by any existing problem in the codebase. It has genuinely different feasibility constraints (x^2 ≡ a mod b with x < c) from all 116 existing problem types. Clear pass.

Correctness

• ✅ Manders & Adleman (1978) — Verified via Semantic Scholar and ScienceDirect: "NP-Complete Decision Problems for Binary Quadratics," Journal of Computer and System Sciences 16, pp. 168–184. The paper proves NP-completeness via reduction from SAT (originally presented at STOC 1976). The issue's citation is correct.
• ✅ Garey & Johnson (1979) — The problem definition matches GJ A7 AN1. The "Extra Remark" section correctly quotes the GJ commentary about polynomial-time solvability when c = ∞ with factorization, and under ERH when b is prime.
• ✅ Examples numerically verified via Python script:
  • Positive: a=2, b=7, c=6 → x=3 satisfies 3²=9≡2 (mod 7). Also x=4 satisfies 4²=16≡2 (mod 7).
  • Negative: a=3, b=7, c=7 → QR mod 7 = {1, 2, 4}, so 3 is a non-residue. No solution exists.

Well-written

Failures:

1. Exponential variable domain breaks dims() contract. The variable x ranges over {1, ..., c−1}. Since input is binary-encoded, c can be exponential in the bit-length (up to 2^64 for u64). The Problem trait's dims() method returns Vec<usize>, which the brute-force solver enumerates exhaustively. For large c, dims() → vec![c - 1] would create an astronomically large search space. The issue must address this impedance mismatch — e.g., by explicitly restricting to small c for testing, or by documenting that brute-force is pseudo-polynomial and only practical for small instances.

2. No concrete declare_variants! complexity string. The complexity section discusses O(c · polylog(b)) but does not provide a concrete expression in terms of getter-accessible parameters (e.g., "c" or "2^num_bits"). The declare_variants! macro requires a compile-time string referencing getter methods.

3. Incomplete worked example. The "Solution search" stops at x=3 without checking x=4 and x=5. Python verification shows x=4 is also a solution (4² = 16 ≡ 2 mod 7). A fully worked example must enumerate all candidates or explicitly state "we stop at the first solution found."

4. Missing getter method names in Schema. The overhead system and declare_variants! require getter methods. The issue should specify what getters the struct provides (e.g., a(), modulus(), upper_bound()). Note: b() as a method name is problematic in Rust.

Warnings (non-blocking):

• The issue does not explore ILP formulation feasibility. Modular arithmetic is not naturally linearizable, so the unchecked ILP box should be explicitly marked infeasible with a brief note.
• Schema uses single-letter field names (a, b, c) which may cause naming conflicts. Consider target_residue, modulus, upper_bound.

Recommendations

• Address the exponential domain issue by adding a paragraph to the Schema section acknowledging the pseudo-polynomial nature and restricting practical brute-force to small c (e.g., c ≤ 10^6).
• Provide a concrete declare_variants! complexity string. Since the brute-force bound is O(c), and c is representable as an input field, consider "upper_bound" (pseudo-polynomial) or express in terms of input bit-length.
• Complete the worked example by showing all 5 evaluations (x=1 through x=5) or noting that the search can stop early.
• Rename schema fields to avoid single-letter conflicts: target_residue, modulus, upper_bound.

[isPANN]

Fix-issue changelog

• Replaced small example (a=2, b=7, c=6 with missed x=4 solution) with richer instance (a=4, b=15, c=10)
• New example has 3 solutions and 6 non-solutions out of 9 candidates — better for testing
• Added negative example (a=3, b=7 — 3 is not a QR mod 7)
• Added explicit dims() note: [c-1] is valid for representable instances; large c is expected NP-hardness
• Added getter methods (a(), b(), c())
• Added complexity string c for declare_variants!
• Added explicit problem type: satisfaction, Value = Or
• Noted ILP is not directly applicable (quadratic constraint)
• Removed "Unverified" markers from verified content

Applied by /fix-issue.