What the name means

QF means quantifier-free: the formula has no explicit 'for every' or 'there exists' binders. IDL means integer difference logic.

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

A difference constraint compares the gap between two values with a fixed amount. The rule finish − start ≤ 4 says that the gap is at most four whole units. Integer variables can take negative values unless a constraint rules them out.

Constraints can be joined with 'and', 'or', and 'not'. Each arithmetic comparison has the restricted difference form. That restriction lets a solver treat many timing problems as a graph of upper bounds on gaps.

Worked example

Fit a job between two events

Let start and finish be integer times. A job takes at least three units, and at most five units may pass between its start and finish.

  1. Write start − finish ≤ −3 for the minimum duration.
  2. Write finish − start ≤ 5 for the maximum duration.
  3. Choose start = 0 and finish = 3. The differences are −3 and 3, so both bounds hold.

The constraints are sat: the chosen times give a model, meaning an assignment that makes every constraint true.

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

Replace the maximum duration with two units. Adding start − finish ≤ −3 and finish − start ≤ 2 gives 0 ≤ −1. The changed query is unsat.

Use cases

  • Check whether whole-tick event timestamps can meet a set of deadlines.
  • Check relative positions in a layout when every distance is an integer and comparisons only bound gaps.

Modeling caution

A rule such as 2 × start + finish ≤ 10 is linear, but it is not a difference constraint. Use QF_LIA when arbitrary fixed coefficients are needed.

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 has no row in the site's retained regression scoreboard. Consult the engine's support documentation for the relevant route.

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.