The nice thing about DTPs is that they are easily generated, given basically one parameter called n, and that trivial instances, both sat- and unsatisfiable, as well as extremely hard ones, can be generated in no time.
A number of solvers are nowadays aimed at the DTP --- some of them are more general, but perform well as well. See the solvers section for a list of them.
Disjunctive Temporal Problems are generated randomly via a simple PERL script, which is available by clicking here. The script requires any standard PERL implementation and is invoked like this:
DTPgen.pl k n m L seed, where
k is the number of disjuncts per clause (forced to be 2)
n is the number of variables
m is the number of clauses
L is the bound on the constant term (usually 100)
seed is the random seed.
A typical output DTP will look like this:
claudio@turing % DTPgen.pl 2 5 10 100 666 # # A random Disjunctive Temporal Problem # # k = 2 literals per clause, # n = 5 arithmetic vars, # m = 10 clauses, # L = 100 is the coefficients' range, # random seed is 666 # x3-x1<=68 v x1-x3<=-15 ^ x0-x3<=42 v x0-x1<=80 ^ x0-x4<=-42 v x2-x4<=34 ^ x3-x2<=-60 v x0-x2<=15 ^ x0-x3<=-60 v x0-x4<=-4 ^ x4-x3<=21 v x1-x4<=-18 ^ x2-x4<=50 v x1-x4<=-20 ^ x4-x0<=-38 v x3-x4<=50 ^ x0-x1<=52 v x1-x0<=27 ^ x0-x1<=88 v x0-x3<=82
where all symbols have the standard meaning (^ and v stand for OR and AND).
In other words, a DTP is a 2CNF having m clauses; every disjunct is a separation predicate xi - xj <= r where xi and xj are distinct variables chosen randomly from a set having n elements and r is an integer chosen uniformly randomly in [-L,L]. Moreover, a check is performed so that no clause is redundant, e.g., x4-x5 <= 3 ^ x4-x5 <= 3.
Usually L is fixed to 100 and m is chosen to range between 2n and 14n; in the end a DTP is characterised by the number of variables, n. The figure below shows a sample plot for n=20:
In the above graph, the x-axis shows the ratio of clauses to variables m/n, varying from 2 to 14, and the y-axis shows the number of consistency checks, that is, calls to an underlying machine for checking that a conjunction of difference constraints is consistent or not.
Recently [PT03], the fairness of this quantity has been put to the test and basically rejected, so that nowadays CPU time is the preferred index of performance.
Usually each point in the graph is the median of 100 randomly generated instances, as it happens in most SAT experimental evaluations.
Check out the related bibliography.