1
$\begingroup$

I want convert timetable scheduling problems to SAT problems. Suppose there are $t$ time slots and $c$ classes. I will define $t\times c$ variables $x_{ij}$, which is true iff class $j$ takes place in time slot $i$. My problem is: suppose there is a constraint that class $a$ takes place after class $b$. How to encode that efficiently in CNF?

$\endgroup$

1 Answer 1

1
$\begingroup$

Variable $a_i$ set means class $a$ is in timeslot $i$, with a similar encoding for class $b$. Higher values of $i$ means later time slots. If class $a$ must occur before class b then you need clauses to declare that exactly one of $a_i$ or $b_{i+1}$, $b_{i+2}$ ... is set. You need one such declaration for each $a_i$ possibility. E.g.

ExactlyOne($a_1, b_2, b_3, b_4, ...$)

ExactlyOne($a_2, b_3, b_4, b_5, ...$)

ExactlyOne($a_3, b_4, b_5, b_6, ...$)

which is efficiently encoded using commander variable encoding as described in Efficient CNF Encoding for Selecting 1 to N Objects. The scheme requires $O(n)$ clause growth, unlike the naive encoding method which requires $O(n^2)$ clause growth.

$\endgroup$
4
  • $\begingroup$ Sorry I don’t follow your reasoning. Suppose $a_1$ and $b_2$ are true, then none of the ExactlyOne clauses will be true. What are you trying to specify here? $\endgroup$
    – Zirui Wang
    Commented Dec 14, 2019 at 8:22
  • $\begingroup$ I'd misremembered something I worked on earlier. I've replaced my broken encoding with a link to an efficient coding scheme. $\endgroup$
    – Kyle Jones
    Commented Dec 16, 2019 at 8:54
  • $\begingroup$ I think it should be $(a_1 \land (b_2 \lor b_3 \lor \cdots)) \lor (a_2 \land (b_3 \lor b_4 \lor \cdots)) \lor \cdots$. But will turning this to CNF result in an efficient encoding? I’m too lazy to work. $\endgroup$
    – Zirui Wang
    Commented Dec 16, 2019 at 10:40
  • $\begingroup$ Yes, CNF clause growth is quadratic as the number of ordering restrictions and time slots increase. The paper I linked to offers a method with better asymptotic clause growth. $\endgroup$
    – Kyle Jones
    Commented Dec 16, 2019 at 15:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.