From 39419fdf04115243868bd698f28df68d2cece381 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Fri, 13 Jan 2017 23:16:57 +0100 Subject: FoodDelivery: format SMT for 1a to fit on one page --- part2.tex | 42 ++++++++++++++++++------------------------ 1 file 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)} -- cgit v1.2.1