What the name means

QF means quantifier-free. NRA means nonlinear real arithmetic; products may contain more than one unknown.

Quantifier-free formulas have no explicit "for every" or "there exists" binders. They can still contain unknown values that the solver must find.

A polynomial combines fixed coefficients, sums, and powers formed by repeated multiplication. A circle equation such as x × x + y × y = 1 belongs here. Values range over real numbers, including irrational values that cannot be written as a ratio of integers.

Polynomial constraints over reals have complete decision methods in principle, though large inputs can be expensive. Adding sine, logarithms, or arbitrary functions changes the problem class. A solver's timeout is still unknown.

Worked example

Locate a square's side length

A square has area two and a positive real-valued side length.

  1. Let side be real and require side > 0.
  2. Require side × side = 2.
  3. The positive square root of two meets both requirements. Its exact value is irrational; a rounded decimal would only approximate it.

The query is sat over reals. An exact model can describe the value by its defining polynomial and a range that selects its positive root.

This is an authored mathematical example, not captured Axeyum output. Here, sat means the constraints can all hold; unsat means they cannot.

A contrasting case

The equation side × side = −1 is unsat over reals because a real square is nonnegative. Complex numbers would change the answer and the theory.

Use cases

  • Check polynomial geometry, including intersections and distance constraints.
  • Find counterexamples to algebraic inequalities in exact physical models.

Modeling caution

A decimal estimate near a root is not evidence of exact equality. Decide whether the application needs an exact algebraic value or a stated error tolerance.

Axeyum coverage

The examples explain the logic's meaning. They do not establish complete Axeyum support for this division. Acceptance, solving, and evidence coverage depend on the input and the solver route.

This division appears in the site's retained regression scoreboard. Read the individual slices and their source records for the tested scope.

The results page also includes a retained comparison for this division. Its figures apply to the named benchmark list and resource budget.

A solver may return unknown if it cannot settle a query. That result establishes neither sat nor unsat. Parsing a declared logic name alone does not prove support for every formula in it.

Engine support documentation at the site's recorded snapshot, 03ae4a3c9, 2026-10-05.

Definitions and references

Definitions consulted September 6, 2026. The worked examples and use-case explanations are authored for this guide.