What the name means

QF means quantifier-free. NIA means nonlinear integer arithmetic, which permits products of integer unknowns.

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

The area equation width × height = 12 is nonlinear when both dimensions are unknown. Integer values rule out fractional dimensions. They remain unbounded mathematical integers unless the formula adds limits.

General nonlinear integer satisfiability is undecidable: no algorithm can correctly finish every possible input. Small equations can still be solved. A solver may find a model, establish unsat for a supported case, or return unknown.

Worked example

Find whole-number dimensions

A rectangle has area 12. Its whole-number width and height must both exceed one.

  1. Declare integer width and height with width ≥ 2 and height ≥ 2.
  2. Require width × height = 12.
  3. Choose width = 3 and height = 4. Their product is 12 and both lower bounds hold.

The query is sat. The dimensions provide a model that can be checked by multiplication.

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

For an integer x, x × x = 2 is unsat. Integers with absolute value at most one have square at most one; all others have square at least four.

Use cases

  • Check integer dimension and factor constraints in discrete layouts.
  • Analyze products of program counters or loop bounds when the model uses mathematical integers.

Modeling caution

Failure to find a value inside a chosen search range does not prove unsat over all integers. A bounded search must explain why values outside its range can be excluded.

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.