SATencoded AllInterval Series Problems
The AllInterval Series (AIS) problem is an arithmetic problem
first used in [Hoos98] in the context of evaluating SLS algorithms
and now contained in
CSPLIB (prob007).
It is inspired by a wellknown problem occurring in serial musical
composition, which, in its original form,
can be stated in the following way:
Given the twelve standard pitchclasses (c,c#,d, ...),
represented by numbers 0,1,...,11, find a series in which each
pitchclass occurs exactly once and in which the musical
intervals between neighbouring notes cover the full set of
intervals from the minor second (1 semitone) to the
major seventh (11 semitones), i.e., for each of these intervals,
there is a pair of neigbhouring pitchclasses in the series,
between which this interval appears.
These musical allinterval series have a certain prominence
in serial composition; they can be traced back
to Alban Berg and have been extensively studied and used
by Ernst Krenek, e.g., in his orchestral piece op.170,
``Quaestio temporis'' (A Question of Time).
The problem of finding such series can be easily
formulated as an instance of a more general arithmetic problem in
Z_n, the set of integer residues modulo n:
For given positive integer n, find a vector
s = (s_1, ..., s_n), such that
 s is a permutation of Z_n = {0,1,...,n1}; and
 the interval vector
v = (s_2s_1, s_3s_2, ... s_ns_{n1})
is a permutation of Z_n{0} = {1,2,...,n1}.
A vector v satisfying these conditions is called
an allinterval series of size n;
the problem of finding such a series is called the
AllInterval Series Problem of size n.
SAT encoding
The allinterval series problem can be represented as a
Constraint Satisfaction Problem in a rather straightforward way.
Each element of s and v is represented as a variable;
the domains of these variables are Z_n and Z_n{0},
respectively; and the contraint relations encode the
conditions 1. and 2. from the definition given above.
From this CSP formulation, instances of the allinterval series
problem can be easily transformed
into a SAT instance by using essentially the same encoding
as for the Graph Colouring Problem, where each assignment
of a value to a single CSP variable is represented by a
propositional variable; each of the three sets of
constraints from the definition above is represented
by a set of clauses; and two additional sets of clauses
ensure that valid SAT assignments
assign exactly one value to each CSP variable.
Hardness
There is a constructive solution to the AllInterval Series problem
which does not require any search, therefore the pure problem is
inherently easy.
The SAT encoded problems, considering their size, very hard
for local search methods like GSAT or Walksat [Hoos98]
but rather easy for systematic algorithms, such as satz.
Simonis and Beldiceanu showed that using the CHIP CSP solver
on a CSP formulation using global constraints the canonical
solution can be found without search
while finding all solutions is difficult even with the efficient
cycle constraint.
In musical composition, solutions different from the
canonical solution, which has a very regular
interval structure, might be more interesting.
Furthermore, it might be interesting to slightly modify the problem
by adding additional constraints on the structure of the
series.
The allinterval series problem presents several potential
challenge for SAT algorithms:
 for local search algorithms, to find the canonical
as efficiently as when using systematic search;
 for stochastic (systematic or local) search algorithms
to sample the full solution space in a reasonably unbiased way;
 for complete algorithms, to find all solutions (an apparently hard problem,
although the number of solutions is relatively small).
The benchmark instances
The benchmark set provided here contains
the four (satisfiable) SAT instances for n=6,8,10,12.
The larger problem instances
have found to be extremely hard to solve for stateoftheart SLSbased SAT
algorithms [Hoos98], all instances are fairly easy for systematic search.
instance
 n
 vars  clauses

ais6  6
 61  581

ais8  8
 113  1,520

ais10  10
 181  3,151

ais12  12
 265  5,666

Table 1: SATencoded instances of the AllInterval Series problem,
all satisfiable.
Bibliography
[Hoos98]
 Holger H. Hoos
Stochastic Local Search  Methods, Models, Applications.
PhD thesis, CS Department, TU Darmstadt, 1998

See also CSPLIB, prob007.