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
  1. s is a permutation of Z_n = {0,1,...,n-1}; and
  2. 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:

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.