From babcf2fdb249b4b4d79d22b42f50847308f60d18 Mon Sep 17 00:00:00 2001 From: Shay Date: Sun, 7 Jun 2026 07:23:23 -0700 Subject: [PATCH] =?UTF-8?q?feat(constraint):=20exact=20integer=202-var=20s?= =?UTF-8?q?olver=20=E2=80=94=20Cramer's=20rule,=20refusal-first=20(R2=20C3?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit generate/constraint_comprehension/solver.py: solve_two_var_linear (order-independent 2x2 integer Cramer's rule over typed constraints), the solve_two_var_count_weight specialization, and solve/answer_constraint_problem driving it from a ConstraintProblem. Four typed refusals: indistinguishable_weights (det==0), non_integer_solution (numer%det!=0, never rounds), negative_solution, verification_failed (identity backstop). Ties to the C2 gold: solves all 7 solved fixtures to their gold value and refuses all 3 solver_refuses fixtures with EXACTLY the gold-claimed reason (the gold's reason is now solver-verified, not just annotation). Per-refusal meaningful-fail + positive re-substitution. Off-serving. 9 tests. --- generate/constraint_comprehension/__init__.py | 10 ++ generate/constraint_comprehension/solver.py | 106 ++++++++++++++++++ tests/test_constraint_solver.py | 98 ++++++++++++++++ 3 files changed, 214 insertions(+) create mode 100644 generate/constraint_comprehension/solver.py create mode 100644 tests/test_constraint_solver.py diff --git a/generate/constraint_comprehension/__init__.py b/generate/constraint_comprehension/__init__.py index 014f0786..d0f685ac 100644 --- a/generate/constraint_comprehension/__init__.py +++ b/generate/constraint_comprehension/__init__.py @@ -24,6 +24,12 @@ from generate.constraint_comprehension.model import ( Domain, Unknown, ) +from generate.constraint_comprehension.solver import ( + answer_constraint_problem, + solve_constraint_problem, + solve_two_var_count_weight, + solve_two_var_linear, +) __all__ = [ "AttributeFact", @@ -34,4 +40,8 @@ __all__ = [ "LinearExpr", "Relation", "Unknown", + "answer_constraint_problem", + "solve_constraint_problem", + "solve_two_var_count_weight", + "solve_two_var_linear", ] diff --git a/generate/constraint_comprehension/solver.py b/generate/constraint_comprehension/solver.py new file mode 100644 index 00000000..4a2bc193 --- /dev/null +++ b/generate/constraint_comprehension/solver.py @@ -0,0 +1,106 @@ +"""Independent exact integer solver for the R2 two-variable linear system. + +Solves a two-variable, two-equation integer linear system by **exact Cramer's rule** — no +floats, no nearest-option snapping. The R2 analogue of the relational-metric answer oracle: +an independent decision procedure that consumes the *structured* constraints, never the text. + +Refusal-first (the wrong=0 boundary). The four ways a count/weight system has no honest +nonnegative-integer answer each REFUSE with a typed reason, never a guessed value: + +- ``indistinguishable_weights`` — the system is singular (``det == 0``): the two equations + cannot separate the unknowns (e.g. equal per-category coefficients), so no unique solution. +- ``non_integer_solution`` — Cramer's numerator is not divisible by the determinant: + no integer solution exists; the solver refuses rather than round. +- ``negative_solution`` — a solved value is negative: invalid in the count domain. +- ``verification_failed`` — a defensive re-substitution backstop (an algebraic identity + for the closed-form Cramer solution, so unreachable while the derivation is correct; retained + as a structural guard against future edits, NOT claimed as an independently-triggerable gate). + +The convenience ``solve_two_var_count_weight`` is the canonical ``x + y = N`` / +``a·x + b·y = T`` specialization; ``solve_constraint_problem`` / ``answer_constraint_problem`` +drive it from a typed :class:`ConstraintProblem`. Off-serving: imports no +``generate.derivation`` / ``core.reliability_gate``. Deterministic; no clock, no randomness. +""" + +from __future__ import annotations + +from generate.constraint_comprehension.expr import LinearConstraint, LinearExpr +from generate.constraint_comprehension.model import ConstraintProblem +from generate.meaning_graph.reader import Refusal + + +def _coeffs(constraint: LinearConstraint, x: str, y: str) -> tuple[int, int, int]: + """``(coeff_x, coeff_y, rhs - lhs_constant)`` for ``constraint`` over the variables x, y.""" + cx = cy = 0 + for symbol, coeff in constraint.lhs.terms: + if symbol == x: + cx += coeff + elif symbol == y: + cy += coeff + return cx, cy, constraint.rhs - constraint.lhs.constant + + +def solve_two_var_linear( + c0: LinearConstraint, c1: LinearConstraint, *, nonnegative: bool = True +) -> dict[str, int] | Refusal: + """Solve a 2-variable, 2-equation integer system over the SAME two symbols by Cramer's rule. + + Precondition (guaranteed upstream by the C2 setup validator / the reader): both constraints + are ``eq`` over exactly two shared symbols. Returns ``{symbol: value}`` or a typed + :class:`Refusal` carrying one of the four solver reasons. + """ + symbols = sorted({s for c in (c0, c1) for s, _ in c.lhs.terms}) + if len(symbols) != 2: # contract violation — upstream must guarantee two variables + raise ValueError(f"solver expects exactly two variables; got {symbols}") + x, y = symbols + p, q, r0 = _coeffs(c0, x, y) + r, s, r1 = _coeffs(c1, x, y) + + det = p * s - q * r + if det == 0: + return Refusal("indistinguishable_weights", f"singular system over {x}/{y}") + num_x = r0 * s - q * r1 + num_y = p * r1 - r0 * r + if num_x % det != 0 or num_y % det != 0: + return Refusal("non_integer_solution", f"no integer solution for {x}/{y}") + vx, vy = num_x // det, num_y // det + if nonnegative and (vx < 0 or vy < 0): + return Refusal("negative_solution", f"{x}={vx}, {y}={vy}") + if p * vx + q * vy != r0 or r * vx + s * vy != r1: # pragma: no cover - identity backstop + return Refusal("verification_failed", "solution failed re-substitution") + return {x: vx, y: vy} + + +def solve_two_var_count_weight( + x: str, y: str, total_count: int, x_weight: int, y_weight: int, weighted_total: int +) -> dict[str, int] | Refusal: + """The canonical specialization: ``x + y = total_count`` and + ``x_weight·x + y_weight·y = weighted_total``. ``x`` / ``y`` are the symbol names.""" + count = LinearConstraint(LinearExpr(((x, 1), (y, 1))), "eq", total_count) + weighted = LinearConstraint(LinearExpr(((x, x_weight), (y, y_weight))), "eq", weighted_total) + return solve_two_var_linear(count, weighted) + + +def solve_constraint_problem(problem: ConstraintProblem) -> dict[str, int] | Refusal: + """Solve a two-constraint :class:`ConstraintProblem`'s system (order-independent).""" + if len(problem.constraints) != 2: # contract violation — upstream guarantees two + raise ValueError(f"solver expects exactly two constraints; got {len(problem.constraints)}") + return solve_two_var_linear(problem.constraints[0], problem.constraints[1]) + + +def answer_constraint_problem(problem: ConstraintProblem) -> int | Refusal: + """Solve, then project to the asked unknown's value (or propagate the refusal).""" + solution = solve_constraint_problem(problem) + if isinstance(solution, Refusal): + return solution + if problem.query.symbol not in solution: # pragma: no cover - query is a category (C2) + return Refusal("query_target_unsolved", problem.query.symbol) + return solution[problem.query.symbol] + + +__all__ = [ + "answer_constraint_problem", + "solve_constraint_problem", + "solve_two_var_count_weight", + "solve_two_var_linear", +] diff --git a/tests/test_constraint_solver.py b/tests/test_constraint_solver.py new file mode 100644 index 00000000..31c26f7d --- /dev/null +++ b/tests/test_constraint_solver.py @@ -0,0 +1,98 @@ +"""Tests for the R2 exact integer solver (C3). + +Ties the solver to the C2 gold: every ``solved`` fixture computes its ``gold`` and every +``solver_refuses`` fixture refuses with EXACTLY the reason the gold claims (so the gold's +stated refusal reason is not just an annotation — the independent solver agrees). Each of the +three reachable refusals is proven meaningful-fail, and every solution is re-substituted into +its constraints (the verification backstop, exercised positively). +""" + +from __future__ import annotations + +from evals.constraint_oracle.runner import _load_r2_gold, gold_to_problem +from evals.constraint_oracle.signature import canonical_constraint +from generate.constraint_comprehension.solver import ( + answer_constraint_problem, + solve_constraint_problem, + solve_two_var_count_weight, + solve_two_var_linear, +) +from generate.meaning_graph.reader import Refusal + + +def _solved() -> list[dict]: + return [f for f in _load_r2_gold() if f["expect"] == "solved"] + + +def _solver_refuses() -> list[dict]: + return [f for f in _load_r2_gold() if f["expect"] == "solver_refuses"] + + +def test_solver_solves_every_solved_gold_to_its_gold_value() -> None: + for fx in _solved(): + problem = gold_to_problem(fx) + got = answer_constraint_problem(problem) + assert got == fx["gold"], f"{fx['id']}: got {got!r}, gold {fx['gold']!r}" + + +def test_solver_solution_satisfies_both_constraints() -> None: + # The verification backstop, exercised positively: the solved values re-substitute exactly. + for fx in _solved(): + problem = gold_to_problem(fx) + sol = solve_constraint_problem(problem) + assert isinstance(sol, dict), fx["id"] + for c in problem.constraints: + terms, _rel, rhs = canonical_constraint(c) + assert sum(coeff * sol[s] for s, coeff in terms) == rhs + + +def test_solver_refuses_every_solver_refuse_gold_with_its_claimed_reason() -> None: + for fx in _solver_refuses(): + problem = gold_to_problem(fx) + got = answer_constraint_problem(problem) + assert isinstance(got, Refusal), f"{fx['id']} should refuse" + assert got.reason == fx["solver_reason"], f"{fx['id']}: {got.reason} != {fx['solver_reason']}" + + +def test_count_weight_convenience_matches_buses() -> None: + assert solve_two_var_count_weight("large_bus", "small_bus", 6, 50, 30, 260) == { + "large_bus": 4, + "small_bus": 2, + } + + +def test_solver_is_constraint_order_independent() -> None: + fx = next(f for f in _solved() if f["id"] == "r2-002-chickens") + p = gold_to_problem(fx) + swapped = solve_two_var_linear(p.constraints[1], p.constraints[0]) + assert swapped == solve_two_var_linear(p.constraints[0], p.constraints[1]) == {"chicken": 11, "cow": 7} + + +# --- meaningful-fail: each reachable refusal fires under exactly its violation --------- # + + +def test_indistinguishable_weights_refuses() -> None: + # Equal coefficients -> singular system -> no unique solution. + out = solve_two_var_count_weight("car", "truck", 8, 4, 4, 32) + assert isinstance(out, Refusal) and out.reason == "indistinguishable_weights" + + +def test_non_integer_solution_refuses() -> None: + # 3*pen + 5*notebook = 37, pen+notebook=10 -> pen = 6.5: refuse, never round. + out = solve_two_var_count_weight("pen", "notebook", 10, 3, 5, 37) + assert isinstance(out, Refusal) and out.reason == "non_integer_solution" + + +def test_negative_solution_refuses() -> None: + # 50*large + 30*small = 400, large+small=6 -> small=-5: refuse. + out = solve_two_var_count_weight("large_bus", "small_bus", 6, 50, 30, 400) + assert isinstance(out, Refusal) and out.reason == "negative_solution" + + +def test_exact_integer_path_is_not_rounded() -> None: + # A near-miss that would round to a plausible integer: 3x+5y=38, x+y=10 -> x=6 exactly. + # (Guards that the solver computes exactly, not by snapping 37/38/39 to the same answer.) + assert solve_two_var_count_weight("x", "y", 10, 3, 5, 38) == {"x": 6, "y": 4} + assert isinstance( + solve_two_var_count_weight("x", "y", 10, 3, 5, 37), Refusal + ) # one less dollar -> no integer split