FoodDelivery: format SMT for 1a to fit on one page

1 files changed, 18 insertions, 24 deletions

diff --git a/part2.tex b/part2.tex
index d140546..75f9f60 100644
--- a/part2.tex
+++ b/part2.tex
@@ -184,36 +184,30 @@ in such a way that each of the villages can consume one food packge forever.
 :extrafuns (
 (s0_0 Int) (s1_0 Int) ... (s4_0 Int) (l0 Int)
 ...
-(s0_30 Int) (s1_30 Int) ... (s4_30 Int) (l30 Int)
 )
 :formula (and
 (= l0 0)
-(= s1_0 80) (= s2_0 80) (= s3_0 80) (= s4_0 80)
-(= s0_0 240)
-(>= s0_0 0)
+(= s1_0 80) (= s2_0 80) (= s3_0 80) (= s4_0 80) (= s0_0 240) (>= s0_0 0)
 (>= s1_0 0) (<= s1_0 120) (>= s2_0 0) (<= s2_0 160)
 (>= s3_0 0) (<= s3_0 100) (>= s4_0 0) (<= s4_0 160)
 ...
-(or
-  (and (= l0 0) (= l1 1)
-       (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
-       (>= (- s0_0 s0_1) 0)
-       (= s1_1 (+ (- s1_0 15) (- s0_0 s0_1)))
-       (= s2_1 (- s2_0 15))
-       (= s3_1 (- s3_0 15))
-       (= s4_1 (- s4_0 15)))
-  ...
-  (and (= l0 1) (= l1 0)
-       (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
-       (= s1_1 (- s1_0 15))
-       (= s2_1 (- s2_0 15))
-       (= s3_1 (- s3_0 15))
-       (= s4_1 (- s4_0 15))
-       (= s0_1 240))
-  ...
-)
-...
-))
+(or (and (= l0 0) (= l1 1)
+         (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
+         (>= (- s0_0 s0_1) 0)
+         (= s1_1 (+ (- s1_0 15) (- s0_0 s0_1)))
+         (= s2_1 (- s2_0 15))
+         (= s3_1 (- s3_0 15))
+         (= s4_1 (- s4_0 15)))
+    ...
+    (and (= l0 1) (= l1 0)
+         (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
+         (= s1_1 (- s1_0 15))
+         (= s2_1 (- s2_0 15))
+         (= s3_1 (- s3_0 15))
+         (= s4_1 (- s4_0 15))
+         (= s0_1 240))
+    ...
+) ...))
 \end{lstlisting}
 
 \subsubsection*{(b)}