# Encoding order relations in CNF

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?

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.

• 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? Commented Dec 14, 2019 at 8:22
• I'd misremembered something I worked on earlier. I've replaced my broken encoding with a link to an efficient coding scheme. Commented Dec 16, 2019 at 8:54
• 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. Commented Dec 16, 2019 at 10:40
• 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. Commented Dec 16, 2019 at 15:57