Class Scheduling to Boolean satisfiability [Polynomial-time reduction]

by

I am going to try and first formalize the problem, and then attempt to reduce it to SAT.

Define the class scheduling problem as:

Input = { S1,S2,....,Sn | Si = {(x_i1, y_i1), (x_i2, y_i2) , ... , (x_ik, y_ik) | 0 <= x_ij < y_ij <= M } }

Informally: The input is a set of classes, each class is a set of (open) intervals in the form (x,y)

(M is some constant that describes the “end of the week”)

Output: True if and only if there exists some set:

R = { (x_1j1, y_1j1) , ..., (x_njn, y_njn) | for each a,b: (x_aja,y_aja) INTERSECTION (x_bjb,y_bjb) = {} }

Informally: true if and only if there is some assignment of intervals such that the intersection between each pair of intervals is empty.

Reduction to SAT:

Define a boolean variable for each interval, V_ij

Based on it, define the formula:

F1 = (V_11 OR V_12 OR ... OR V_1(k_1)) AND .... AND (V_n1 OR V_n2 OR ... OR V_n(k_n))

Informally, F1 is satisfied if and only if at least one of the interval for each class is “satisfied”

Define Smaller(x,y) = true if and only if x <= y1

We will use it to make sure intervals don’t overlap.

Note that if we want to make sure (x1,y1) and (x2,y2) don’t overlap, we need:

x1 <= y1 <= x2 <= y2 OR  x2 <= y2 <= x1 <= y1

Since the input guarantees x1<=y1, x2<=y2, it reduces to:

y1<= x2 OR y2 <= x1

And using our Smaller and boolean clauses:

Smaller(y1,x2) OR Smaller(y2,x1)

Now, let’s define new clauses to handle with it:

For each pair of classes a,b and intervals c,d in them (c in a, d in b)

G_{c,d} = (Not(V_ac) OR Not(V_bd) OR Smaller(y_ac,x_bd) OR Smaller(y_bd,x_ac))

Informally, if one of the intervals b or d is not used – the clause is satisfied and we are done. Otherwise, both are used, and we must ensure there is no overlap between the two intervals.

This guarantees that if both c,d are “chosen” – they do not overlap, and this is true for each pair of intervals.

Now, form our final formula:

F = F1 AND {G_{c,d} | for each c,d}

This formula ensures us:

  1. For each class, at least one interval is chosen
  2. For each two intervals c,d – if both c and d are chosen, they do not overlap.

Small note: This formula allows to chose more than 1 interval from each class, but if there is a solution with some t>1 intervals, you can easily remove t-1 of them without changing correctness of the solution.

At the end, the chosen intervals are the boolean variables V_ij we defined.

Example:

Alebgra = {(1,3),(3,5),(4,6)} Calculus = {(1,4),(2,5)}

Define F:

F1 = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2)

Define G’s:

G{A1,C1} = Not(V1,1) OR Not(V2,1) OR  4 <= 1 OR 3 <= 1 //clause for A(1,3) C(1,4)
         = Not(V1,1) OR Not(V2,1) OR false = 
         = Not(V1,1) OR Not(V2,1)
G{A1,C2} = Not(V1,1) OR Not(V2,2) OR  3 <= 2 OR 5 <= 1 // clause for A(1,3) C(2,5)
         = Not(V1,1) OR Not(V2,2) OR false = 
         = Not(V1,1) OR Not(V2,2)
G{A2,C1} = Not(V1,2) OR Not(V2,1) OR  5 <= 1 OR 4 <= 3 //clause for A(3,5) C(1,4)
         = Not(V1,2) OR Not(V2,1) OR false = 
         = Not(V1,2) OR Not(V2,1)
G{A2,C2} = Not(V1,2) OR Not(V2,2) OR  5 <= 2 OR 5 <= 3 // clause for A(3,5) C(2,5)
         = Not(V1,2) OR Not(V2,2) OR false = 
         = Not(V1,2) OR Not(V2,2)
G{A3,C1} = Not(V1,3) OR Not(V2,1) OR  4 <= 4 OR 6 <= 1 //clause for A(4,6) C(1,4)
         = Not(V1,3) OR Not(V2,1) OR true= 
         = true
G{A3,C2} = Not(V1,3) OR Not(V2,2) OR  6 <= 2 OR 5 <= 4 // clause for A(4,6) C(2,5)
         = Not(V1,3) OR Not(V2,2) OR false = 
         = Not(V1,3) OR Not(V2,2)

Now we can show our final formula:

    F = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2) 
        AND  Not(V1,1) OR Not(V2,1) AND Not(V1,1) OR Not(V2,2)
        AND  Not(V1,2) OR Not(V2,1) AND Not(V1,2) OR Not(V2,2)
        AND  true AND Not(V1,3) OR Not(V2,2)

The above is satisfied only when:

V1,1 = false
V1,2 = false
V1,3 = true
V2,1 = true
V2,2 = false

And that stands for the schedule: Algebra=(4,6); Calculus=(1,4), as desired.

(1) can be computed as a constant to the formula pretty easily, there are polynomial number of such constants.

Leave a Comment