What the name means

QF means quantifier-free. LIA means linear integer arithmetic: unknowns are whole numbers, and multiplication uses fixed coefficients.

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

An integer is a whole number, positive, zero, or negative. Integer arithmetic has no fixed word size, so addition does not wrap at a machine limit. A count of people needs an explicit nonnegative bound.

Linear expressions include 3 × vans + cars. The three is fixed. Multiplying two unknowns, such as vans × trips, needs nonlinear arithmetic. 'Linear' describes the arithmetic; the formula can still contain alternatives and conditions.

Worked example

Choose vehicles for a group

A van seats six people and a car seats four. A group needs at least 14 seats, using at most three vehicles.

  1. Let vans and cars be nonnegative integers.
  2. Require 6 × vans + 4 × cars ≥ 14 and vans + cars ≤ 3.
  3. Choose vans = 1 and cars = 2. The total is 14 seats in three vehicles.

The query is sat. It establishes a valid choice, without proving that the choice is cheapest or best.

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 2 × vans = 3 is unsat over integers. Replacing integers with reals would admit vans = 1.5 and change the problem.

Use cases

  • Check staffing or packing rules that count indivisible items.
  • Find inputs that reach a program branch when its conditions use mathematical integer sums and fixed multiples.

Modeling caution

Optimization is a separate request. A satisfying model need not minimize cost. Also check the exact logic definition before using division or remainder: parser extensions can exceed the declared fragment.

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.