[Model] QuadraticDiophantineEquations

[isPANN]

Motivation

QUADRATIC DIOPHANTINE EQUATIONS (P227) from Garey & Johnson, A7 AN8. An NP-complete number-theoretic problem: given positive integers a, b, c, determine whether there exist positive integers x and y such that ax^2 + by = c. This result by Manders and Adleman (1978) is a landmark in computational complexity, showing that even simple Diophantine equations with just two unknowns and degree two are NP-complete. This contrasts with the polynomial-time solvability of purely linear Diophantine equations (sum of a_ix_i = c) and pure power equations (ax^k = c). The general Diophantine problem (arbitrary polynomial, arbitrary many variables) is undecidable (Matiyasevich's theorem, extending MRDP), but restricting to a single nonlinear variable keeps the problem in NP.

Associated reduction rules:

• As source: [Rule] QUADRATIC DIOPHANTINE EQUATIONS to SIMULTANEOUS DIVISIBILITY OF LINEAR POLYNOMIALS #555 (QUADRATIC DIOPHANTINE EQUATIONS -> SIMULTANEOUS DIVISIBILITY OF LINEAR POLYNOMIALS)
• As target: [Rule] 3SAT to QUADRATIC DIOPHANTINE EQUATIONS #560 (3SAT -> QUADRATIC DIOPHANTINE EQUATIONS)

Definition

Name: QuadraticDiophantineEquations

Reference: Garey & Johnson, Computers and Intractability, A7 AN8

Mathematical definition:

INSTANCE: Positive integers a, b, and c.
QUESTION: Are there positive integers x and y such that ax^2 + by = c?

Variables

• Count: 1 (the quadratic unknown x; the linear unknown y is determined by x)
• Per-variable domain:
  • x: {1, 2, ..., floor(sqrt(c/a))} -- since ax^2 <= c, x is bounded by sqrt(c/a)
• Meaning: x is the variable appearing quadratically in the equation. Given x, the linear variable y = (c - ax^2) / b is uniquely determined; a configuration is feasible iff (c - ax^2) > 0 and (c - a*x^2) mod b == 0 (yielding a positive integer y).
• dims() implementation: vec![floor(sqrt(c / a)) as usize] -- config [i] maps to x = i + 1 (1-indexed). The brute-force solver enumerates only x; y is derived, not searched.

Schema (data type)

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

Field	Type	Description
a	u64	Coefficient of x^2
b	u64	Coefficient of y
c	u64	Right-hand side constant

Size fields (getters): a, b, c -- the three coefficients are the natural size parameters. Reduction overhead expressions reference these directly (e.g., rule #560 derives bit_length_b = O(n log n) from the product of n primes encoded in b).

Complexity

• Best known exact algorithm: For each candidate x in {1, ..., floor(sqrt(c/a))}, check if (c - ax^2) is positive and divisible by b, yielding y = (c - ax^2)/b. This runs in O(sqrt(c/a) * polylog(c)) time, which is pseudo-polynomial. The problem is NP-complete because c (and hence sqrt(c/a)) can be exponential in the input bit-length. Purely linear Diophantine equations are solvable in polynomial time using the extended Euclidean algorithm. The NP-hardness comes from the interaction of the quadratic term with the linear term and the positivity constraints. [Manders and Adleman, JCSS 16:168-184, 1978.]
• Complexity string: "sqrt(c)"

Extra Remark

Full book text:

INSTANCE: Positive integers a, b, and c.
QUESTION: Are there positive integers x and y such that ax^2 + by = c?

Reference: [Manders and Adleman, 1978]. Transformation from 3SAT.
Comment: Diophantine equations of the forms ax^k = c and Sigma_{i=1}^{k} a_i*x_i = c are solvable in polynomial time for arbitrary values of k. The general Diophantine problem, "Given a polynomial with integer coefficients in k variables, does it have an integer solution?" is undecidable, even for k = 13 [Matijasevic and Robinson, 1975]. However, the given problem can be generalized considerably (to simultaneous equations in many variables) while remaining in NP, so long as only one variable enters into the equations in a non-linear way (see [Gurari and Ibarra, 1978]).

How to solve

• It can be solved by (existing) bruteforce. (Enumerate x from 1 to floor(sqrt(c/a)); for each x, check if (c - ax^2) > 0 and (c - ax^2) mod b == 0, yielding y = (c - a*x^2)/b.)
• It can be solved by reducing to integer programming. (ILP with integer variables x, y >= 1 and equality constraint ax^2 + by = c; however, the quadratic term makes this a mixed-integer quadratic program.)
• Other: The problem can be reduced to Quadratic Congruences (P220) by observing that ax^2 + by = c iff ax^2 ≡ c (mod b) with x bounded by sqrt(c/a).

Example Instance

Input:
a = 3, b = 5, c = 53

Question: Are there positive integers x, y with 3x^2 + 5y = 53?

Solution search:

• dims() = [floor(sqrt(53/3))] = [4], so x ranges from 1 to 4 (config indices 0..3).
• x = 1 (config [0]): 3*1 + 5y = 53 => 5y = 50 => y = 10. YES! (x=1, y=10)
• x = 2 (config [1]): 3*4 + 5y = 53 => 5y = 41 => y = 8.2. Not integer.
• x = 3 (config [2]): 3*9 + 5y = 53 => 5y = 26 => y = 5.2. Not integer.
• x = 4 (config [3]): 3*16 + 5y = 53 => 5y = 5 => y = 1. YES! (x=4, y=1)

Answer: YES. Two solutions: (x=1, y=10) and (x=4, y=1).

Verification of (x=4, y=1): 3*(4^2) + 5*1 = 48 + 5 = 53 = c.

Negative example:
a = 3, b = 5, c = 10

• dims() = [floor(sqrt(10/3))] = [1], so x = 1 only.
• x = 1: 3 + 5y = 10 => 5y = 7 => y = 1.4. Not integer.
• No solution exists. Answer: NO.

[zazabap]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but currently an orphan node — neither associated reduction target/source exists in the codebase
Non-trivial	✅ Pass	Genuinely distinct number-theoretic decision problem, not isomorphic to any existing model
Correctness	✅ Pass	Manders & Adleman (1978) verified; Garey & Johnson A7 AN8 reference is accurate
Well-written	⚠️ Warn	Minor issues with variable mapping to the codebase's trait system

Overall: 2 passed, 0 failed, 2 warnings

---

Usefulness

The problem QuadraticDiophantineEquations does not exist in the codebase — it is a novel addition. The motivation is well-written and explains the significance of this problem in computational complexity theory (landmark result showing even simple degree-2 Diophantine equations are NP-complete).

However, the associated reduction rules (R166: QDE -> SimultaneousDivisibility, R171: 3SAT -> QDE) reference problems that also do not exist in the codebase. This means the problem would initially be an orphan node in the reduction graph with no connections. The issue would benefit from specifying which existing codebase problem it could connect to (e.g., a reduction from KSatisfiability).

Non-trivial

This is a genuinely distinct problem. The only existing number-theoretic problem is Factoring, which has a completely different structure (finding multiplicative factors vs. satisfying a mixed quadratic-linear equation with positivity constraints). The feasibility constraint ax^2 + by = c with x, y > 0 is unique among all existing models. Pass.

Correctness

• Manders & Adleman (1978): Verified. The paper "NP-Complete Decision Problems for Binary Quadratics" (JCSS 16:168-184) proves NP-completeness of deciding whether ax^2 + by = c has positive integer solutions. This matches the issue's claims.
• Garey & Johnson A7 AN8: The issue's "Extra Remark" section reproduces the book text accurately, including the reference to Matijasevic and Robinson (1975) for undecidability of general Diophantine problems, and Gurari and Ibarra (1978) for the generalization.
• Complexity analysis: The pseudo-polynomial brute-force argument is correct — enumerating x up to sqrt(c/a) is O(sqrt(c/a)) which is exponential in the input bit-length. The NP-completeness claim is sound.
• 3SAT transformation: The issue mentions "Transformation from 3SAT" which is consistent with Manders and Adleman's original reduction.

Well-written

Strengths:

• Excellent motivation section with proper context (polynomial-time solvability of linear and pure-power cases, undecidability of general case)
• Well-worked example with both positive (a=3, b=5, c=53) and negative (a=3, b=5, c=10) instances
• Full verification of solutions shown

Issues to address:

1. Variable mapping to trait system: The issue describes 2 variables (x, y) with heterogeneous domains, but in the codebase's Problem trait, dims() returns per-variable domain sizes. The issue should clarify how dims() would work — likely vec![floor(sqrt(c/a)) as usize, floor((c-a)/b) as usize] — and note that both variables are 1-indexed (positive integers), which differs from the typical 0-indexed binary variables.

2. Missing getter methods / size fields: The overhead system requires getter methods for complexity expressions. The issue should specify what getters the type will expose (e.g., bit_length() for the input bit-length, or a(), b(), c() for the coefficients). This is important for declare_variants! complexity strings.

3. Complexity string unclear: The issue describes the brute-force complexity but does not propose a concrete complexity string for declare_variants!. Since the best known algorithm is essentially brute-force enumeration of x values, the complexity would need to be expressed in terms of input bit-length (e.g., "2^(bit_length / 2)" or similar).

4. ILP solver path: The issue correctly notes the quadratic term prevents direct ILP formulation, but the checkbox is unchecked without a clear alternative solver path beyond brute force.

Recommendations

• Add a concrete declare_variants! complexity string proposal
• Specify getter methods for the overhead system
• Clarify the dims() implementation strategy for heterogeneous variable domains
• Consider whether a connection to an existing problem (e.g., KSatisfiability/3SAT) could be implemented alongside the model to avoid an orphan node

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but orphan node — neither associated rule's source/target exists in the codebase yet
Non-trivial	✅ Pass	Genuinely distinct number-theoretic problem; no isomorphic existing model
Correctness	✅ Pass	Manders & Adleman (1978) verified; Matiyasevich & Robinson (1975) verified
Well-written	⚠️ Warn	Missing concrete complexity string for declare_variants!; missing size field getter specification; dims() strategy unclear

Overall: 2 passed, 0 failed, 2 warnings

Re-check (previous report: 2026-03-12). Previously: 2 warnings → Now: 2 warnings (same items remain unaddressed).

---

Usefulness

QuadraticDiophantineEquations does not exist in the codebase — it is a novel addition. The motivation is excellent, placing the problem in context between polynomial-time linear Diophantine equations and undecidable general Diophantine equations.

However, the associated reduction rules (R166: QDE → SimultaneousDivisibility, R171: 3SAT → QDE) reference problems that do not exist in the codebase. The problem would be an orphan node with no connections to the existing reduction graph. The issue would benefit from specifying a concrete path to an existing problem (e.g., a reduction from KSatisfiability).

Non-trivial

The only existing number-theoretic problem is Factoring, which has a completely different structure (multiplicative factorization vs. mixed quadratic-linear Diophantine equation with positivity constraints). The feasibility constraint ax² + by = c with x, y > 0 is unique among all ~60 existing models. Pass.

Correctness

References verified:

Reference	Verdict
Manders & Adleman, "NP-Complete Decision Problems for Binary Quadratics", JCSS 16:168–184, 1978	✅ Confirmed — paper exists, proves NP-completeness of ax² + by = c
Garey & Johnson A7 AN8	✅ Book text accurately reproduced in the issue
Matiyasevich & Robinson (1975), undecidability with k=13 unknowns	✅ Confirmed — "Reduction of an arbitrary Diophantine equation to one in 13 unknowns", Acta Arithmetica XXVII:521–549
Gurari & Ibarra, generalization to many variables with one nonlinear	✅ Paper confirmed (actual publication year 1979 in JACM 26(3):567–581, but G&J cites it as 1978 which the issue correctly quotes)

Minor note on reduction origin: The issue quotes G&J's "Transformation from 3SAT." The original Manders-Adleman paper uses a generic NDTM simulation proof rather than an explicit 3SAT reduction. This is G&J's standard shorthand — not an error in the issue.

Example verification (Python script):

Example 1: a=3, b=5, c=53
  x=1: 3·1² + 5·10 = 53 ✓  (solution)
  x=2: remainder 41, not divisible by 5
  x=3: remainder 26, not divisible by 5
  x=4: 3·16 + 5·1 = 53 ✓   (solution)
  → 2 solutions out of 40 (x,y) pairs. Matches issue. ✅

Example 2: a=3, b=5, c=10
  x=1: remainder 7, not divisible by 5
  → No solutions. Matches issue. ✅

Both examples verified correct. The positive example has 2 feasible and 38 infeasible configurations — adequate for round-trip testing of a satisfaction problem.

Well-written

Strengths:

• Excellent motivation with proper complexity-theoretic context
• Well-worked examples with both positive and negative instances, step-by-step verification
• Negative example included — good for testing
• Full G&J book text reproduced for reference

Issues to address:

1. Missing concrete complexity string for declare_variants!: The issue describes O(√(c/a) · polylog(c)) brute-force but doesn't propose a complexity expression in terms of getter methods. Since this is pseudo-polynomial (exponential in input bit-length), the codebase needs something like "sqrt(c)" or a bit-length-based expression. Suggest adding a Complexity string field.

2. Missing size field / getter specification: The overhead system requires getter methods (e.g., a(), b(), c(), or bit_length()). The issue should specify which getters the type will expose, as reduction overhead expressions reference them.

3. dims() implementation strategy unclear: The Problem trait requires dims() -> Vec<usize>. For this problem, dims() would be vec![floor(√(c/a)), floor((c−a)/b)], but the y-domain can be O(c) — exponentially large in input bit-length. For large instances, the generic brute-force solver (which enumerates the Cartesian product of dims()) would be impractical. The issue should discuss whether a custom solver strategy is needed or whether dims() should only represent the x-variable (since y is determined by x).

Recommendations

• Add a concrete declare_variants! complexity string proposal (e.g., "sqrt(c)")
• Specify getter methods for the type (at minimum a(), b(), c())
• Clarify the dims() strategy — recommend vec![floor(sqrt(c/a))] (1 variable: x) since y is uniquely determined by x, making the search space O(√(c/a)) rather than the Cartesian product
• Consider linking a concrete reduction to an existing problem to avoid orphan status

[isPANN]

Fix-issue changelog

• Associated rules: Replaced G&J rule numbers (R166, R171) with GitHub issue cross-references ([Rule] QUADRATIC DIOPHANTINE EQUATIONS to SIMULTANEOUS DIVISIBILITY OF LINEAR POLYNOMIALS #555, [Rule] 3SAT to QUADRATIC DIOPHANTINE EQUATIONS #560)
• Variables: Reduced from 2 variables to 1 (x only; y is derived). Added dims() implementation: vec![floor(sqrt(c/a))] with config-to-variable mapping
• Schema: Added "Size fields (getters)" paragraph specifying a, b, c
• Complexity: Added concrete complexity string "sqrt(c)" with citation
• Example: Added dims() annotations and config indices to the solution search

Applied by /fix-issue.