Encoding Class Disjunctive Scheduling

Class Tree
Description Given a set of task intervals each of which has a fixed duration, an earliest start time, and a latest end time; a set of precedence constraints each of which states that one task must be completed before another; and a set of disjunctive constraints each of which states that two task intervals cannot overlap each other. The goal of disjunctive scheduling is to assign a start time (an integer) to each task such that the given constraints are all satisfied.

Input format

The input file contains the following atoms:

a. There is an atom in the form task(Ii,Di) for each task interval that specifies the identifier Ii and the duration Di (an integer).

task(I1,D1). task(I2,D2). ... task(In,Dn).

b.There is an atom in the form est(Ii,Si) for each task interval that specifies the earliest start time Si (an integer) for task Ii.

c. There is an atom in the form let(Ii,Ei) for each task interval that specifies the latest end time Ei (an integer) for task Ii.

d. A binary relation prec/2 that specifies the precedence relationship. An atom prec(I,J) in the relation states that task I is required to precede task J.

e. A binary relation disj/2 that specifies the non-overlapping task intervals. An atom disj(I,J) states that task I and task J cannot overlap.

Output format

The output is a binary relation time/2 if there is a solution. There is an atom time(Ii,Ti) for each task which means that the start time for task Ii is Ti. For each task Ii, let Si be the earliest start time, Di the duration, Ei the latest end time. The solution must satisfy the following constraints:

a. Ti>=Si and Ti+Di=<Ei.

b. For each input atom prec(Ii,Ij), Ti+Di=<Tj.

c. For each input atom disj(Ii,Ij), Ti+Di=<Tj or Tj+Dj=<Ti.

The output should be UNSATISFIABLE if there is no solution that satisfies all the constraints.

Sample input

task(a_a,60). task(a_n,30). task(a_o,2). task(a_s,5). task(b_a,75). task(b_n,3). task(b_o,15). task(b_s,10). task(c_a,5). task(c_n,15). task(c_o,10). task(c_s,30). task(d_a,90). task(d_n,1). task(d_o,1). task(d_s,1).

est(a_a,700). est(a_n,700). est(a_o,700). est(a_s,700). est(b_a,715). est(b_n,715). est(b_o,715). est(b_s,715). est(c_a,715). est(c_n,715). est(c_o,715). est(c_s,715). est(d_a,800). est(d_n,800). est(d_o,800). est(d_s,800).

let(a_a,1000). let(a_n,1000). let(a_o,1000). let(a_s,1000). let(b_a,1000). let(b_n,1000). let(b_o,1000). let(b_s,1000). let(c_a,1000). let(c_n,1000). let(c_o,1000). let(c_s,1000). let(d_a,1000). let(d_n,1000). let(d_o,1000). let(d_s,1000).

disj(a_a,a_n). disj(a_a,a_o). disj(a_a,a_s). disj(a_n,a_o). disj(a_n,a_s). disj(a_o,a_s). disj(b_a,b_n). disj(b_a,b_o). disj(b_a,b_s). disj(b_n,b_o). disj(b_n,b_s). disj(b_o,b_s). disj(c_a,c_n). disj(c_a,c_o). disj(c_a,c_s). disj(c_n,c_o). disj(c_n,c_s). disj(c_o,c_s). disj(d_a,d_n). disj(d_a,d_o). disj(d_a,d_s). disj(d_n,d_o). disj(d_n,d_s). disj(d_o,d_s). disj(a_a,b_a). disj(a_a,c_a). disj(a_a,d_a). disj(b_a,c_a). disj(b_a,d_a). disj(c_a,d_a). disj(a_n,b_n). disj(a_n,c_n). disj(a_n,d_n). disj(b_n,c_n). disj(b_n,d_n). disj(c_n,d_n). disj(a_o,b_o). disj(a_o,c_o). disj(a_o,d_o). disj(b_o,c_o). disj(b_o,d_o). disj(c_o,d_o). disj(a_s,b_s). disj(a_s,c_s). disj(a_s,d_s). disj(b_s,c_s). disj(b_s,d_s). disj(c_s,d_s).

Sample output

time(a_a,890). time(a_n,700). time(a_o,730). time(a_s,745). time(b_a,715). time(b_n,815). time(b_o,790). time(b_s,805). time(c_a,790). time(c_n,745). time(c_o,760). time(c_s,715). time(d_a,800). time(d_n,890). time(d_o,891). time(d_s,892).

Authors: Neng-Fa Zhou
Affiliation: CUNY Brooklyn College
Encodings
1 - 2 of 2