SAT-encoded All-Interval Series Problems
The All-Interval 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 well-known problem occurring in serial musical
composition, which, in its original form,
can be stated in the following way:
Given the twelve standard pitch-classes (c,c#,d, ...),
represented by numbers 0,1,...,11, find a series in which each
pitch-class 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 pitch-classes in the series,
between which this interval appears.
These musical all-interval 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,...,n-1}; and
- the interval vector
v = (|s_2-s_1|, |s_3-s_2|, ... |s_n-s_{n-1}|)
is a permutation of Z_n-{0} = {1,2,...,n-1}.
A vector v satisfying these conditions is called
an all-interval series of size n;
the problem of finding such a series is called the
All-Interval Series Problem of size n.
SAT encoding
The all-interval 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 all-interval 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 All-Interval 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 all-interval 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 state-of-the-art SLS-based 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: SAT-encoded instances of the All-Interval 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.