Class Scheduling to Boolean satisfiability [Polynomial-time reduction]

Question

I have some theoretical/practical problem and I don't have clue for now on how to manage, Here it is:

I create a SAT solver able to find a model when one is existing and to prove the contradiction when it's not the case on CNF problems in C using genetics algorithms.

A SAT-problem looks basically like this kind of problem : My goal is to use this solver to find solutions in a lot of different NP-completes problems. Basically, I translate different problems into SAT, solve SAT with my solver and then transform the solution into a solution acceptable for the original problem.

I already succeed for the N*N Sudoku and also the N-queens problems, but here is my new goal : to reduce the Class Scheduling Problem to SAT but I have no idea how to formalize a class-scheduling problem in order to easily transform it in SAT after.

The goal is obviously, in few months, to generate a picture of a schedule like this one :

I found this source-code who is able to solved the class-scheduling but without any reductions to SAT unfortunately :/

I also found some articles about Planning in general (http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf for instance).

But the planning domain definition language used in this article seems quite too general for me to represents a Class-scheduling problem. :/

Does someone has an idea on how to formalize efficiently a Class-scheduling in order to reduce it to SAT and after, transform the SAT solution (if it exists ^^) into a Class-schedule ?

I'm basically open to any suggestions, I for now have no idea on how to represents, how to reduce the problem, how to transform the SAT-solution into a schedule...

---

Follow up question: Class Scheduling to Boolean satisfiability [Polynomial-time reduction] part 2

Answer 1

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 <= y¹
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.