Polynomial solving: refuse questions with no algorithm¶

Some requests look like ordinary computations but have no program that answers them correctly for every input. "Does this polynomial equation with integer coefficients have a solution in rational numbers?" is one of them once the equation has several variables: a service that tries to answer it by searching can run forever, holding a worker until a timeout fires and the client retries. This page shows how the library's router refuses that request immediately, what the refusal does and does not mean, and what your service should offer instead. It assumes you run or design a computer-algebra feature, not that you know computability theory.

At a glance


Question	Should a "solve this polynomial over the rationals" endpoint accept arbitrary multivariable polynomials?
Owner	Owners of a computer-algebra system (CAS), a notebook "solve" button, or a symbolic-regression feature.
Today's habit	Start a search over ever-larger fractions and put a timeout around it.
What this adds	A router request, `rational_zeros`, that always comes back at once with `ok=False` and the reason, and never starts a search.
Demo outcome	The request for \(x^3 + y^3 - 3xyz - 1 = 0\) is refused in microseconds, even though the caller tagged it as solvable.
Kind of example	A router refusal, not a decision: there is no act/abstain verdict.
Example id	`hilbert_refuse` (`uv run grounded-decision examples hilbert_refuse`)

For a review slide: "We do not offer a complete rational solver for arbitrary polynomials; we offer exact answers for one variable and a bounded, explicitly incomplete search for more."

The question today¶

A client submits an equation such as \(x^3 + y^3 - 3xyz - 1 = 0\) and asks whether it has a solution with \(x, y, z\) rational numbers. The endpoint has to answer "yes" (ideally with a solution), "no", or nothing.

How hard that is depends on the shape of the input:

One variable. Easy and complete. The rational root theorem limits candidate solutions to a finite list (divisors of the constant term over divisors of the leading coefficient); check each.
Several variables, integer solutions. No complete algorithm exists. This is Hilbert's tenth problem, proved unsolvable by Matiyasevich in 1970 building on Davis, Putnam and Robinson: no program answers "is there an integer solution?" correctly for every equation.
Several variables, rational solutions. The case this endpoint serves. See the status note below; either way, no complete algorithm is available to ship.

Where today's habit goes wrong¶

The naive endpoint searches fractions with larger and larger numerators and denominators. If a solution exists it may eventually find one. If none exists, the search never ends, so the endpoint cannot ever answer "no". In production that looks like a worker held until a timeout, a client retry, and a queue filling with searches that will never return. A timeout does not fix this: it turns "no answer" into "no answer after 30 seconds".

The demo equation shows the other half of the problem. It has obvious rational solutions (\(x = 1, y = 0\), any \(z\)), which a short search finds at once. Finding a solution is easy for some inputs; promising an answer for every input is what cannot be done.

What the library will and will not claim¶

The router says	It does not say
A `rational_zeros` request is refused: `ok=False`, envelope `undec` ("no complete procedure").	That this particular equation has no solution. It never reads the equation.
The refusal is immediate and the same for every input, whatever envelope the caller asked for.	That a bounded or special-case search is wrong. Those are different, honest products.
The reason, with a reference to the math catalog entry it relies on.	That the reason is machine-checked. The catalog entry is marked `lean=False`.

Status of the underlying result

In the wider literature: whether there is an algorithm that decides if a polynomial equation with integer coefficients has a rational solution (Hilbert's tenth problem over \(\mathbb{Q}\)) has long been treated as an open problem. The integer version is settled (undecidable).

In this project's math catalog: a negative resolution over \(\mathbb{Q}\) is recorded from a manuscript (catalog result 004). This package marks it lean=False: it is published in the catalog but not machine-checked here.

The product conclusion does not depend on which reading is right. If the problem is undecidable, no complete solver exists; if it is open, nobody knows one. Either way a service cannot promise a complete answer today. See where each result stands.

The router's refusal is broader than the mathematics: it refuses without parsing, so even a one-variable equation sent as rational_zeros is refused. Handle the easy cases yourself before calling it (see Wiring it in).

Data you provide¶

Input	Source	Notes
The equation text	Client request	Passed as `{"poly": text}`. The router does not read it.
Number of variables	Your parser	Decides whether to solve exactly yourself or route to the refusal.
Search bound and time	Your product	Only for the separate, bounded endpoint.

Worked example¶

The demo sends one request, tagged P_EXACT ("solvable exactly in polynomial time"), the way an optimistic caller would. The router overrides the tag and refuses: ok=False, envelope undec, detail "no complete algorithm for integer polynomials over Q (catalog 004)". No worker was started and nothing about the polynomial was computed.

The numbers (from uv run grounded-decision examples hilbert_refuse --json)

Field	Value
`subgoal`	`rational_zeros`
`envelope`	`undec` (the caller asked for `p_exact`)
`ok`	false
`detail`	`no complete algorithm for integer polynomials over Q (catalog 004)`
`value.family`	`004`
`value.lean`	false

If the caller tags the request UNDEC itself, the dispatcher refuses one step earlier, before the handler, with detail="envelope UNDEC: refuse" and value=None. The outcome is the same; the different strings tell you in logs which layer refused.

What your service does with the result¶

Return an error the client will not retry. HTTP 422 with the envelope and detail, and "retryable": false.
Offer the honest alternatives: an exact answer for one variable, and a bounded search for more. A bounded search may answer "yes, here is a solution" (a found solution is a correct answer) or "none found up to height \(H\) within \(T\) seconds". It must never answer "no".
Branch on ok, not on an exception. dispatch does not raise for this request. There is no decision record on this path.

Tuning and monitoring¶

There is nothing to tune in the refusal. For the bounded endpoint, choose the height \(H\) (largest numerator and denominator tried) and time limit \(T\) from your latency budget, and state both in every response.

Limits and risks¶

The router refuses every rational_zeros request, including ones that are easy (one variable, or with a small obvious solution).
The status of the rational case is contested between the wider literature and the catalog; the refusal is a product policy that is correct under either reading.
Special classes of equations (quadratic forms, many curves) have algorithms. Supporting them is a separate feature with its own justification, not a branch inside rational_zeros.

Wiring it in¶

from grounded_decision.router import Subgoal, dispatch
from grounded_decision.types import Envelope


def solve_over_rationals(polynomial_text: str):
    polynomial = parse(polynomial_text)  # your CAS parser
    if len(polynomial.variables) == 1:
        # Complete and exact: rational root theorem.
        return {"complete": True, "roots": rational_roots_univariate(polynomial)}
    router_result = dispatch(
        Subgoal("rational_zeros", Envelope.P_EXACT, {"poly": polynomial_text})
    )
    if not router_result.ok:
        return error_response(  # your web framework
            status=422,
            body={
                "envelope": router_result.envelope.value,
                "detail": router_result.detail,
                "retryable": False,
                "alternative": "/solve/bounded",
            },
        )

parse, rational_roots_univariate and error_response are your functions. Dispatch before allocating a worker, log router_result.to_dict(), and count refusals per client to see who needs the bounded endpoint.

Run it yourself¶

uv run grounded-decision examples hilbert_refuse

The output prints the submitted equation and the requested tag, then one block: what arrived (INPUT), what the naive endpoint would do (NAIVE), the router's refusal and why (DECISION), the result fields (OUTPUT) and what the service does next. Add --json for the raw result.