diff options
Diffstat (limited to 'part2.tex')
-rw-r--r-- | part2.tex | 42 |
1 files changed, 18 insertions, 24 deletions
@@ -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)} |