Name  Sample Instances  # of Instances  SAT/UNSAT  Description  

lengthsshort 
first.smt20
first.smt25 last.smt20 last.smt25 
100  sat  Each instance has 30 variables. Each variable’s length is constrained randomly from 0 to X.


lengthslong 
first.smt20
first.smt25 last.smt20 last.smt25 
100  sat  Each instance has 30 variables. Each variable’s length is constrained randomly from 0 to X.


lengthsconcats 
first.smt20
first.smt25 last.smt20 last.smt25 
100  sat  Each instance has X variables, and Y random unique binary concats of those variables.


concatssmall 
first.smt20
first.smt25 last.smt20 last.smt25 
60  sat  Each instance is a rightheavy concat tree of depth X,
equal to the string


concatsbig 
first.smt20
first.smt25 last.smt20 last.smt25 
60  sat  Each instance is a rightheavy concat tree of depth X,
equal to the string


concatsbalanced 
first.smt20
first.smt25 last.smt20 last.smt25 
100  sat  Each instance is a balanced concat tree of depth X,
equal to the string


concatsextractssmall 
first.smt20
first.smt25 last.smt20 last.smt25 
60  both  Each instance is a rightheavy concat tree of depth 30,
equal to the string


concatsextractsbig 
first.smt20
first.smt25 last.smt20 last.smt25 
60  both  Each instance is a rightheavy concat tree of depth 30,
equal to the string


overlapssmall 
first.smt20
first.smt25 last.smt20 last.smt25 
60  both  Each instance is an equation of the form a.V = V.b, where V is a concatenation of X variables.


overlapsbig 
first.smt20
first.smt25 last.smt20 last.smt25 
20  both  Each instance is an equation of the form a.V = V.b, where V is a concatenation of X variables.


regexsmall 
first.smt20
first.smt25 last.smt20 last.smt25 
60  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.


regexbig 
first.smt20
first.smt25 last.smt20 last.smt25 
60  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.


regexdeep 
first.smt20
first.smt25 last.smt20 last.smt25 
45  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.


manyregexes 
first.smt20
first.smt25 last.smt20 last.smt25 
40  both  Each instance tests whether a variable is in X regexes. Each regex is a concatenation of 10 terms of depth 2.


regexpair 
first.smt20
first.smt25 last.smt20 last.smt25 
40  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.


regexlengths 
first.smt20
first.smt25 last.smt20 last.smt25 
40  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.


differentprefix 
first.smt20
first.smt25 last.smt20 last.smt25 
60  unsat  Each instance is a problem of the form V = a.Y = b.Y where V is a variable.
