SMT logics explained

What SMT means

Satisfiability modulo theories, abbreviated SMT, asks whether a set of constraints can all hold under specified mathematical rules. A constraint is a condition, such as a start time being at least two. A theory supplies rules for values and operations, such as integer addition or array reads.

Boolean satisfiability, abbreviated SAT, uses variables that are true or false. SMT adds values such as integers, strings, and machine bit patterns. It retains their meaning: the solver knows that an integer cannot be both below two and above five. Each value has a sort, meaning its kind of value.

A logic fragment specifies which sorts, operations, and forms of statement a formula may use. A benchmark division groups problems by such a fragment. The division name helps identify suitable solving methods. It does not state how quickly a particular solver will finish.

A job that must finish on time

A machine becomes available at hour two. A new job takes one hour and must finish by hour four. Its start time must be a whole hour. These are linear integer constraints: start ≥ 2 and start + 1 ≤ 4.

(set-logic QF_LIA)
(declare-const start Int)
(assert (>= start 2))
(assert (<= (+ start 1) 4))
(check-sat)

SMT-LIB defines a shared language for writing solver queries. Here, set-logic names the fragment, declare-const introduces the unknown start time, and each assert adds a constraint. check-sat asks whether they can all hold. Parentheses put the operation first: (+ start 1) means start + 1.

The assignment start = 2 meets both conditions: 2 ≥ 2 and 2 + 1 ≤ 4. It is a model, meaning values that make all the constraints true. A start at hour three also works. The query asks for a valid schedule; it does not ask for the earliest schedule.

sat

The constraints can all hold. A model shows a suitable assignment.

unsat

The constraints cannot all hold under the stated rules. If the deadline were hour two, the job could not fit.

unknown

The solver has not settled the question, perhaps because of a time limit or an unsupported solving method. This is no conclusion about whether a schedule exists.

To check a claimed property, ask for a case that violates it. A sat result supplies a counterexample to inspect. An unsat result establishes that no such case meets the encoded assumptions. It says nothing about requirements omitted from the formula.

Read a logic name

In QF_UFLIA, QF means quantifier-free, UF means uninterpreted functions, and LIA means linear integer arithmetic. An uninterpreted function has no supplied implementation, but it must give the same output for the same input. Linear arithmetic permits fixed multiples such as 3 × x; multiplying two unknowns, x × y, requires nonlinear arithmetic.

QF

No explicit quantifiers such as "for every x" or "there exists y".

A / AX

Arrays: indexed collections with read, write, and equality rules.

UF

Uninterpreted functions and, where allowed, abstract sorts.

BV

Bit-vectors: fixed-width strings of bits with machine-style operations.

FP

Floating-point values with specified precision and rounding.

LIA / LRA

Linear integer arithmetic / linear real arithmetic.

NIA / NRA

Nonlinear integer arithmetic / nonlinear real arithmetic.

IDL / RDL

Difference logic: comparisons that bound the gap between two integer or real values.

S / SEQ

Strings / sequences. The sequence label and accepted declarations vary by solver.

DT / FF

Datatypes built from constructors / finite fields with their own arithmetic.

A quantifier binds a variable and states whether a condition holds for every value or for at least one value. Quantifier-free formulas can still contain unknowns. In the schedule above, start is an unknown whose value the solver seeks. The prefix QF does not mean variable-free or easy.

Without QF, a logic such as BV or LIA permits explicit quantifiers. Their order matters: "for every input, some response works" lets the response depend on the input. "One response works for every input" requires a single shared response.

The names have historical exceptions. For example, QF_AUFLIA restricts arrays to integer indices and integer elements. Check the SMT-LIB logic definitions for the exact restrictions; concatenating letter groups does not define a new standard logic.

Choose values that match the problem

Choose the smallest fragment that expresses the intended rules. Add nonnegative bounds, valid-index conditions, and overflow behavior when the application needs them. Changing the declaration alone does not translate a formula into that fragment.

Check the implementation separately

A logic definition describes valid formulas. It does not establish that a solver accepts every operation, decides every input, or produces independently checkable evidence. Axeyum's coverage varies by route. Its parser records the declared logic, while its dispatcher chooses a route from the parsed terms.

A benchmark result belongs to a particular file list, solver version, and resource budget. A small example in these guides is a mathematical exercise, not a measured Axeyum result. See the reference index for support and evidence documentation, or continue with the SMT solving lesson to follow the solver's internal steps.