All problems in one archive can be found here: problems.zip.

Name Sample Instances # of Instances SAT/UNSAT Description
lengths-short first.smt20
first.smt25
last.smt20
last.smt25
50 sat

Each instance has 30 variables. Each variable’s length is constrained randomly from 0 to X.

X 1 ≤ X ≤ 251 in increments of 5.
lengths-long first.smt20
first.smt25
last.smt20
last.smt25
50 sat

Each instance has 30 variables. Each variable’s length is constrained randomly from 0 to X.

X 1 ≤ X ≤ 5001 in increments of 100.
lengths-concats first.smt20
first.smt25
last.smt20
last.smt25
50 sat

Each instance has X variables, and Y random unique binary concats of those variables.

X 10 ≤ X ≤ 510 in increments of 1.
Y 1 ≤ Y ≤ 51 in increments of 1.
concats-small first.smt20
first.smt25
last.smt20
last.smt25
50 sat

Each instance is a right-heavy concat tree of depth X, equal to the string "solution".

X 1 ≤ X ≤ 51 in increments of 1.
concats-big first.smt20
first.smt25
last.smt20
last.smt25
30 sat

Each instance is a right-heavy concat tree of depth X, equal to the string "solution".

X 1 ≤ X ≤ 1201 in increments of 40.
concats-balanced first.smt20
first.smt25
last.smt20
last.smt25
10 sat

Each instance is a balanced concat tree of depth X, equal to the string "solution".

X 1 ≤ X ≤ 11 in increments of 1.
concats-extracts-small first.smt20
first.smt25
last.smt20
last.smt25
50 sat

Each instance is a right-heavy concat tree of depth 30, equal to the string "solution", followed by X extracts of 1 character each, from a random index Y.

X 1 ≤ X ≤ 51 in increments of 1.
Y 0 ≤ Y ≤ 100.
concats-extracts-big first.smt20
first.smt25
last.smt20
last.smt25
30 sat

Each instance is a right-heavy concat tree of depth 30, equal to the string "solution", followed by X extracts of 1 character each, from a random index Y.

X 1 ≤ X ≤ 1201 in increments of 40.
Y 0 ≤ Y ≤ 1000.
overlaps-small first.smt20
first.smt25
last.smt20
last.smt25
30 both

Each instance is an equation of the form a.V = V.b, where V is a concatenation of X variables.

X 1 ≤ X ≤ 31 in increments of 1.
overlaps-big first.smt20
first.smt25
last.smt20
last.smt25
10 both

Each instance is an equation of the form a.V = V.b, where V is a concatenation of X variables.

X 1 ≤ X ≤ 151 in increments of 15.
regex-small first.smt20
first.smt25
last.smt20
last.smt25
30 sat

Each instance tests whether a variable belongs to a random regex. The regex is a concatenation of X random regex terms of depth 2.

X 1 ≤ X ≤ 61 in increments of 2.
regex-big first.smt20
first.smt25
last.smt20
last.smt25
30 sat

Each instance tests whether a variable belongs to a random regex. The regex is a concatenation of X random regex terms of depth 2.

X 1 ≤ X ≤ 211 in increments of 7.
regex-deep first.smt20
first.smt25
last.smt20
last.smt25
15 both

Each instance tests whether a variable belongs to a random regex. The regex is a concatenation of 2 random regex terms of depth X. The variable is at least 15 characters long.

X 0 ≤ X ≤ 15 in increments of 1.
many-regexes first.smt20
first.smt25
last.smt20
last.smt25
20 both

Each instance tests whether a variable is in X regexes. Each regex is a concatenation of 10 terms of depth 2.

X 1 ≤ X ≤ 61 in increments of 3.
regex-pair first.smt20
first.smt25
last.smt20
last.smt25
20 both

Each instance tests whether a variable is in one regex but not another. Each regex is a concatenation of X terms of depth 2.

X 1 ≤ X ≤ 101 in increments of 5.
regex-lengths first.smt20
first.smt25
last.smt20
last.smt25
20 both

Each instance tests whether a variable is in a regex, and constrains the variable to a minimum length of X. The regex contains 10 terms, each of depth 2.

X 1 ≤ X ≤ 501 in increments of 25.