What the name means

QF means quantifier-free. S names the string fragment; a string is a finite sequence of characters.

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

Concatenation joins strings in order. A word equation sets two such expressions equal and asks which strings can fill the unknown parts. Pattern constraints can also require membership in a regular language, a set of strings described by a regular expression.

The string theory defines exact operations on characters. It does not silently perform case folding or normalize text. This guide uses QF_S for string-only problems; explicit linear arithmetic over lengths belongs in QF_SLIA.

Worked example

Complete a file name

An unknown stem followed by the suffix '.csv' must equal 'sales.csv'.

  1. Write stem joined with '.csv' = 'sales.csv'.
  2. Assign stem the string 'sales'.
  3. Joining 'sales' and '.csv' gives the required string with the same characters in the same order.

The query is sat. The assignment identifies a string that meets the equation.

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

Require the stem also to equal 'costs'. The joined text becomes 'costs.csv', so the combined query is unsat.

Use cases

  • Find text inputs that pass or violate string-based branch conditions.
  • Check exact prefixes, suffixes, and concatenation rules in a parser model.

Modeling caution

A string equation does not know filesystem case rules, path normalization, or which names are valid on a device. Add those rules when they affect the question.

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.