3jobshop_machine_constraint.smt2

;; Machine 0- only 2 tasks, it's easy
(assert (or
  (and  (<= (+ t00 3) t10))
 (and  (<= (+ t10 2) t00))))

;; Machine 1: three tasks, so 6 possible sequences!
(assert (or
  (and  (<= (+ t01 2) t12) (<= (+ t12 4) t20))
  (and  (<= (+ t01 2) t20) (<= (+ t20 4) t12))
 (and  (<= (+ t12 4) t01) (<= (+ t01 2) t20))
 (and  (<= (+ t12 4) t20) (<= (+ t20 4) t01))
 (and  (<= (+ t20 4) t01) (<= (+ t01 2) t12))
 (and  (<= (+ t20 4) t12) (<= (+ t12 4) t01))))

;; Machine 2 : same problem
(assert (or
  (and  (<= (+ t02 2) t11) (<= (+ t11 1) t21))
 (and  (<= (+ t02 2) t21) (<= (+ t21 3) t11))
 (and  (<= (+ t11 1) t02) (<= (+ t02 2) t21))
 (and  (<= (+ t11 1) t21) (<= (+ t21 3) t02))
 (and  (<= (+ t21 3) t02) (<= (+ t02 2) t11))
 (and  (<= (+ t21 3) t11) (<= (+ t11 1) t02))))