Go to Qiita Advent Calendar 2024 Top
LoginSignup
8
5

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 3 years have passed since last update.

@hanohrs(Hirosato Hano)inNTTデータ先端技術

Microsoft の SMT ソルバー、Z3 でマクドナルドで一日分の栄養を取れる組み合わせを計算してみたら衝撃の結果が・・・出ない！？

Posted at

普段は研究開発の現場で、開発で使う様々なツールを動かす、試験が通っているか確認する、比較のために先行研究のプログラムを条件を整えて動かしてみる、論文にならないようなちょっとしたアルゴリズムの改善をするなど、研究を下支えするエンジニアリングの仕事をしています。

Qiita を始めたので、いつか Z3 の記事を書こうと思っていました。ナンプレか何かでやろうと思っていたところ、恐るべきバズり記事が爆誕したので、予定を変更して「マクドナルド問題」を扱いたいと思います。ここでマクドナルド問題とは、「マクドナルドで一日分の栄養を取れる組み合わせを計算したら衝撃の結果に (2021年02月22日 17時01分 (JST))」のダイエット問題を解き、最高のメニューの中身、つまり何をいくつ食べるのかを求めるものとします。

Z3 はナンプレのような問題には強いですが、果たしてマクドナルド問題を解くことはできるでしょうか？

Microsoft はまだ本気出してないだけ

「マクドナルドで一日分の栄養を取れる組み合わせを計算したら衝撃の結果に」を読んでいたら、衝撃の記述を目にしました。オチではありません。

Excelにもソルバーが搭載されていますが、この程度の数の決定変数でもエラーになって計算できませんでした。

これです！ Excel、そんな子だったの!?

でも、Microsoft はまだ本気出してないだけ。

優秀な研究者を多数抱える Microsoft Research は、Excel をチューリング完全にするなんて朝飯前だし、SMT という種類では最強 [要出典]1 のソルバーを作ることだってできちゃいます。

その名も Z3！

Z3 は与えた論理式を満たす例や満たさない例があり得るのか、あるならその時の変数がどういう組み合わせかを出したりするのが得意です。Java プログラマーに身近なところでは、Eclipse IDE は sat4j というライブラリを内部的に利用して依存関係を解析していますが、そういった SAT ソルバーというものの上位互換です。

SAT/SMT ソルバーの基本を知りたい方は、@masahiro_sakai さんの「SAT/SMTソルバの仕組み」をご覧ください。日本語だからかもしれませんが、私は世界一わかりやすいと思っています。

Z3 には定評があり、Qiita にもそれなりの数の Z3 タグの記事があることからその人気をご理解いただけると思います。最適化問題を解くこともでき2、オマケ機能とはいえ、ダイエット問題ならば解けそうな気がします。

したんですよ、この時点では！

チュートリアルを試す

しかし、私は最適化のために Z3 を使った経験はありません。チュートリアルから理解していきたいと思います。

チュートリアルは rise4fun というサイトにあり、Z3 をブラウザーで動かしながら使い方を学ぶことができます。数理最適化に関しては Z3 - optimization で解説されています。

ダイエット問題はある制約を満たした上で合計カロリーを最小化したいというものですから、その意味では2つ目の minimize を用いる例題と同種です。

(declare-const x Int)
(declare-const y Int)
(assert (< x 4))
(assert (< (- y x) 1))
(assert (> y 1))
(minimize (+ x y))
(check-sat)
(get-objectives)

この Lisp 方言と言って良さそうな記述は、The SMT-LIB language 2.0 (以下 SMTLIB2) という形式です。意味的には以下のような流れになります。

  • 最初の2行で x、y という変数を宣言し
  • 次の3行で満たすべき制約 x < 4、y - x < 1、y > 1 を書き
  • x + y を最小化するという指示を (check-sat) で実行させ
  • (get-objectives) で最終的な状態を取得する

load in editor ボタンを押して右側に読み込ませ、▶️ ボタンを押すと、次の結果が得られました。

sat
(objectives
 ((+ x y) 4)
)

sat、つまり解があったよ (解なしじゃないよ)、その時の x + y は 4 だよ、ということです。

しかし、x と y がそれぞれ具体的にいくらか出してくれないと、マクドナルド問題のソルバーとしては使えませんね。そこで、最後の命令を get-objectives ではなく get-model に変更します。▶️ ボタンを押すと、次の結果が得られました。

sat
(model 
  (define-fun y () Int
    2)
  (define-fun x () Int
    2)
)

これは y = 2、x = 2 という意味です。

正確には、Java で書くと IntSupplier y = () -> 2;、IntSupplier x = () -> 2; というような内容ですが、The SMT-LIB Standard Version 2.6 (PDF) の p. 60 には以下の記述があります。

(declare-const f σ) abbreviates the command (declare-fun f () σ)

x や y は元記事では変数と呼ばれており、これは私の感覚とも一致するのですが、なぜ SMTLIB2 では declare-const で定数 (constant) として宣言するのかは把握できていません。定数は引数のない関数である、というのは Haskell などの遅延評価の関数型言語と共通する部分だと思いますが、Java などとはだいぶ感覚が違います。

マクドナルド問題を解こうとしてみる

チュートリアルで、解けたときの具体的な値を得る方法を習得できました。次はマクドナルド問題に挑戦します。

rise4fun で動かすと迷惑になる計算量かもしれませんので、ダウンロードして動かします。macOS で Z3 の releases ページ から z3-4.8.10-x64-osx-10.15.7.zip をダウンロードして展開しておきます。

% curl -OsSL https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-osx-10.15.7.zip
% unzip -q z3-4.8.10-x64-osx-10.15.7.zip
% cd z3-4.8.10-x64-osx-10.15.7/bin

次に、マクドナルド問題の記事で書かれていた Python のコードを、エディターやスクリプトを駆使して SMTLIB2 形式に置き換えます。

拡張子は smt2 としました。VS Code で smt-lib-syntax という拡張を提案されましたので、一般的に使われる拡張子だと思われます。

ちなみに、栄養素の制約の部分は手作業での変換はつらく、OpenJDK 11 以降のクラス ファイルを作らずに実行する方法で Java を使いました。「これは Java スクリプトですか？」で習得した知識が役立ちました。

prob2smt2.java
import java.io.BufferedReader;
import java.io.InputStreamReader;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

class Prob2Smt2 {
    public static void main(String[] args) {
        Iterable<String> strs = new BufferedReader(new InputStreamReader(System.in)).lines()::iterator;
        for (String str : strs) {
            Pattern p = Pattern.compile("([0-9.]+)\\*([a-z]+)(\\+)?");
            Matcher m = p.matcher(str);
            StringBuilder sb = new StringBuilder();
            sb.append("(assert (>= (+");
            while(m.find()) {
                String c = m.group(2);
                if (c.equals("as"))
                    c = "_as";
                m.appendReplacement(sb, String.format("(* $1 %s)", c));
            }
            m.appendTail(sb);
            String s = sb.toString();
            s = s.replace("prob +=", "").replaceFirst(">= ([0-9.]+)", ") $1))");
            System.out.println(s);
        }
    }
}

ソルバーの入力は以下のようになりました。SMTLIB2 の流儀に従って小文字を使うようにし、as は予約語だったので _as に直しています。

mcdonalds.smt2
;; variables
(declare-const _as Int)
(declare-const aa Int)
(declare-const ab Int)
(declare-const ac Int)
(declare-const ad Int)
(declare-const ae Int)
(declare-const af Int)
(declare-const ag Int)
(declare-const ah Int)
(declare-const ai Int)
(declare-const aj Int)
(declare-const ak Int)
(declare-const al Int)
(declare-const am Int)
(declare-const an Int)
(declare-const ao Int)
(declare-const ap Int)
(declare-const aq Int)
(declare-const ar Int)
(declare-const at Int)
(declare-const au Int)
(declare-const av Int)
(declare-const aw Int)
(declare-const ax Int)
(declare-const ay Int)
(declare-const az Int)
(declare-const ba Int)
(declare-const bb Int)
(declare-const bc Int)
(declare-const bd Int)
(declare-const be Int)
(declare-const bf Int)
(declare-const bg Int)
(declare-const bh Int)
(declare-const bi Int)
(declare-const bj Int)
(declare-const bk Int)
(declare-const bl Int)
(declare-const bm Int)
(declare-const bn Int)
(declare-const bo Int)
(declare-const bp Int)
(declare-const bq Int)
(declare-const br Int)
(declare-const bs Int)
(declare-const bt Int)
(declare-const bu Int)
(declare-const bv Int)
(declare-const bw Int)
(declare-const bx Int)
(declare-const by Int)
(declare-const bz Int)
(declare-const ca Int)
(declare-const cb Int)
(declare-const cc Int)
(declare-const cd Int)
(declare-const ce Int)
(declare-const cf Int)
(declare-const cg Int)
(declare-const ch Int)
(declare-const ci Int)
(declare-const cj Int)
(declare-const ck Int)
(declare-const cl Int)
(declare-const cm Int)
(declare-const cn Int)
(declare-const co Int)
(declare-const cp Int)
(declare-const cq Int)
(declare-const cr Int)
(declare-const cs Int)
(declare-const ct Int)
(declare-const cu Int)
(declare-const cv Int)
(declare-const cw Int)
(declare-const cx Int)
(declare-const cy Int)
(declare-const cz Int)
(declare-const da Int)
(declare-const db Int)
(declare-const dc Int)
(declare-const dd Int)
(declare-const de Int)
(declare-const df Int)
(declare-const dg Int)
(declare-const dh Int)
(declare-const di Int)
(declare-const dj Int)
(declare-const dk Int)
(declare-const dl Int)
(declare-const dm Int)
(declare-const dn Int)
(declare-const do Int)
(declare-const dp Int)
(declare-const dq Int)
(declare-const dr Int)
(assert (and (>= _as 0) (>= aa 0) (>= ab 0) (>= ac 0) (>= ad 0) (>= ae 0) (>= af 0) (>= ag 0) (>= ah 0) (>= ai 0) (>= aj 0) (>= ak 0) (>= al 0) (>= am 0) (>= an 0) (>= ao 0) (>= ap 0) (>= aq 0) (>= ar 0) (>= at 0) (>= au 0) (>= av 0) (>= aw 0) (>= ax 0) (>= ay 0) (>= az 0) (>= ba 0) (>= bb 0) (>= bc 0) (>= bd 0) (>= be 0) (>= bf 0) (>= bg 0) (>= bh 0) (>= bi 0) (>= bj 0) (>= bk 0) (>= bl 0) (>= bm 0) (>= bn 0) (>= bo 0) (>= bp 0) (>= bq 0) (>= br 0) (>= bs 0) (>= bt 0) (>= bu 0) (>= bv 0) (>= bw 0) (>= bx 0) (>= by 0) (>= bz 0) (>= ca 0) (>= cb 0) (>= cc 0) (>= cd 0) (>= ce 0) (>= cf 0) (>= cg 0) (>= ch 0) (>= ci 0) (>= cj 0) (>= ck 0) (>= cl 0) (>= cm 0) (>= cn 0) (>= co 0) (>= cp 0) (>= cq 0) (>= cr 0) (>= cs 0) (>= ct 0) (>= cu 0) (>= cv 0) (>= cw 0) (>= cx 0) (>= cy 0) (>= cz 0) (>= da 0) (>= db 0) (>= dc 0) (>= dd 0) (>= de 0) (>= df 0) (>= dg 0) (>= dh 0) (>= di 0) (>= dj 0) (>= dk 0) (>= dl 0) (>= dm 0) (>= dn 0) (>= do 0) (>= dp 0) (>= dq 0) (>= dr 0)))

;; constraints
(assert (>= (+ (* 12.5 aa) (* 14.5 ab) (* 19 ac) (* 16.7 ad) (* 20.2 ae) (* 15.5 af) (* 22.3 ag) (* 19.2 ah) (* 61.9 ai) (* 19.9 aj) (* 26.5 ak) (* 27.3 al) (* 39.5 am) (* 0 an) (* 14.2 ao) (* 21.5 ap) (* 15 aq) (* 26.5 ar) (* 15.8 _as) (* 17.1 at) (* 14 au) (* 15.2 av) (* 20 aw) (* 12.8 ax) (* 0 ay) (* 34.1 az) (* 26.2 ba) (* 26 bb) (* 14.4 bc) (* 15.9 bd) (* 17.7 be) (* 8 bf) (* 0 bg) (* 17.2 bh) (* 10.4 bi) (* 20.3 bj) (* 15.7 bk) (* 29.7 bl) (* 0 bm) (* 19.4 bn) (* 35.3 bo) (* 25.8 bp) (* 30 bq) (* 33.3 br) (* 39.8 bs) (* 40.6 bt) (* 23.2 bu) (* 42 bv) (* 23.5 bw) (* 26.1 bx) (* 23 by) (* 34.8 bz) (* 20.6 ca) (* 41.4 cb) (* 22.7 cc) (* 25.5 cd) (* 27.2 ce) (* 39 cf) (* 26.7 cg) (* 21.4 ch) (* 32.4 ci) (* 5.2 cj) (* 0.2 ck) (* 3 cl) (* 0.4 cm) (* 0.5 cn) (* 13.4 co) (* 15.3 cp) (* 0.5 cq) (* 15 cr) (* 0.2 cs) (* 14.8 ct) (* 5 cu) (* 3.8 cv) (* 47.3 cw) (* 15.8 cx) (* 0.3 cy) (* 1.2 cz) (* 0.2 da) (* 3.8 db) (* 3.7 dc) (* 1.9 dd) (* 38.2 de) (* 60.6 df) (* 0.4 dg) (* 6.7 dh) (* 5.3 di) (* 2.9 dj) (* 5.9 dk) (* 8 dl) (* 3.2 dm) (* 5.4 dn) (* 5.9 do) (* 5.3 dp) (* 0.4 dq) (* 0.4 dr) ) 39))
(assert (>= (+ (* 17.4 aa) (* 29.4 ab) (* 21.1 ac) (* 20 ad) (* 23.2 ae) (* 30.2 af) (* 18.9 ag) (* 13.5 ah) (* 65.5 ai) (* 21.7 aj) (* 30.7 ak) (* 26.6 al) (* 43.1 am) (* 0 an) (* 20.2 ao) (* 30.6 ap) (* 25.1 aq) (* 25 ar) (* 13.4 _as) (* 23 at) (* 15.5 au) (* 17.3 av) (* 21.9 aw) (* 9.4 ax) (* 6.7 ay) (* 51.3 az) (* 42.7 ba) (* 28.3 bb) (* 13.9 bc) (* 13.3 bd) (* 20.8 be) (* 8.6 bf) (* 0 bg) (* 23.7 bh) (* 23.8 bi) (* 33.2 bj) (* 18.1 bk) (* 49.7 bl) (* 0 bm) (* 25.5 bn) (* 36.1 bo) (* 50 bp) (* 26.5 bq) (* 34.2 br) (* 43.2 bs) (* 39.1 bt) (* 28.7 bu) (* 40.1 bv) (* 21 bw) (* 31.6 bx) (* 24 by) (* 34.7 bz) (* 16.9 ca) (* 43.4 cb) (* 18.6 cc) (* 28.4 cd) (* 43.5 ce) (* 36.2 cf) (* 23.7 cg) (* 38.3 ch) (* 33.1 ci) (* 3 cj) (* 1.5 ck) (* 18 cl) (* 0 cm) (* 0.1 cn) (* 51.8 co) (* 13.1 cp) (* 0.2 cq) (* 12.9 cr) (* 0 cs) (* 12.8 ct) (* 18.9 cu) (* 3.9 cv) (* 51.6 cw) (* 17.2 cx) (* 11.2 cy) (* 9.6 cz) (* 0.1 da) (* 4.4 db) (* 18.1 dc) (* 10.7 dd) (* 60.3 de) (* 103.4 df) (* 2.3 dg) (* 25.9 dh) (* 20.6 di) (* 11.3 dj) (* 7 dk) (* 10.6 dl) (* 0.8 dm) (* 5.5 dn) (* 10.7 do) (* 5.5 dp) (* 10.9 dq) (* 0 dr) ) 75))
(assert (>= (+ (* 47.7 aa) (* 55.8 ab) (* 66.6 ac) (* 48.4 ad) (* 52.4 ae) (* 36.4 af) (* 31 ag) (* 27.1 ah) (* 57.5 ai) (* 38.9 aj) (* 36.8 ak) (* 35.5 al) (* 57.5 am) (* 9.5 an) (* 38.1 ao) (* 27.3 ap) (* 27.2 aq) (* 31.4 ar) (* 30.8 _as) (* 39.2 at) (* 37.7 au) (* 37 av) (* 47.3 aw) (* 30.3 ax) (* 0 ay) (* 92.9 az) (* 40.2 ba) (* 41.8 bb) (* 35.8 bc) (* 26.4 bd) (* 29.1 be) (* 52.7 bf) (* 30.2 bg) (* 34.3 bh) (* 41.9 bi) (* 42.4 bj) (* 42.4 bk) (* 31.2 bl) (* 0.1 bm) (* 62.8 bn) (* 76 bo) (* 44.1 bp) (* 31 bq) (* 38.9 br) (* 36.8 bs) (* 35.5 bt) (* 48 bu) (* 31.4 bv) (* 30.8 bw) (* 49.1 bx) (* 47.6 by) (* 64.4 bz) (* 30.3 ca) (* 41.8 cb) (* 45 cc) (* 29.1 cd) (* 35.5 ce) (* 36.3 cf) (* 38.2 cg) (* 37.6 ch) (* 32.7 ci) (* 9.6 cj) (* 4.3 ck) (* 28.3 cl) (* 5.6 cm) (* 2.3 cn) (* 128.5 co) (* 18.2 cp) (* 1.1 cq) (* 18.3 cr) (* 1.2 cs) (* 17.2 ct) (* 21.1 cu) (* 24.7 cv) (* 39.2 cw) (* 13.1 cx) (* 1.6 cy) (* 13.3 cz) (* 7.7 da) (* 26.4 db) (* 31.5 dc) (* 26.8 dd) (* 90.4 de) (* 167.7 df) (* 5.2 dg) (* 64.3 dh) (* 51 di) (* 28 dj) (* 37.7 dk) (* 53.4 dl) (* 9.7 dm) (* 46.8 dn) (* 44.1 do) (* 40.6 dp) (* 2 dq) (* 1.2 dr) ) 675))
(assert (>= (+ (* 919 aa) (* 986 ab) (* 1296 ac) (* 994 ad) (* 1216 ae) (* 829 af) (* 813 ag) (* 649 ah) (* 2326 ai) (* 816 aj) (* 1052 ak) (* 1129 al) (* 1714 am) (* 4 an) (* 996 ao) (* 789 ap) (* 722 aq) (* 1132 ar) (* 747 _as) (* 1060 at) (* 850 au) (* 813 av) (* 1139 aw) (* 542 ax) (* 36 ay) (* 1673 az) (* 962 ba) (* 1007 bb) (* 644 bc) (* 636 bd) (* 837 be) (* 711 bf) (* 1 bg) (* 890 bh) (* 971 bi) (* 1193 bj) (* 1030 bk) (* 1358 bl) (* 254 bm) (* 1309 bn) (* 2082 bo) (* 1308 bp) (* 965 bq) (* 987 br) (* 1223 bs) (* 1300 bt) (* 1501 bu) (* 1435 bv) (* 898 bw) (* 1565 bx) (* 1355 by) (* 1778 bz) (* 693 ca) (* 1310 cb) (* 816 cc) (* 989 cd) (* 1142 ce) (* 1428 cf) (* 1340 cg) (* 1245 ch) (* 1554 ci) (* 84 cj) (* 2 ck) (* 222 cl) (* 210 cm) (* 1 cn) (* 830 co) (* 791 cp) (* 152 cq) (* 730 cr) (* 91 cs) (* 639 ct) (* 55 cu) (* 83 cv) (* 1517 cw) (* 506 cx) (* 283 cy) (* 307 cz) (* 182 da) (* 318 db) (* 154 dc) (* 217 dd) (* 1426 de) (* 2346 df) (* 182 dg) (* 415 dh) (* 329 di) (* 181 dj) (* 155 dk) (* 268 dl) (* 37 dm) (* 135 dn) (* 118 do) (* 118 dp) (* 222 dq) (* 384 dr) ) 5000))
(assert (>= (+ (* 119 aa) (* 237 ab) (* 328 ac) (* 212 ad) (* 343 ae) (* 255 af) (* 297 ag) (* 183 ah) (* 860 ai) (* 366 aj) (* 432 ak) (* 379 al) (* 536 am) (* 7 an) (* 262 ao) (* 235 ap) (* 170 aq) (* 358 ar) (* 232 _as) (* 277 at) (* 246 au) (* 258 av) (* 345 aw) (* 214 ax) (* 0 ay) (* 730 az) (* 477 ba) (* 372 bb) (* 198 bc) (* 148 bd) (* 230 be) (* 254 bf) (* 0 bg) (* 266 bh) (* 167 bi) (* 256 bj) (* 172 bk) (* 415 bl) (* 2 bm) (* 138 bn) (* 610 bo) (* 433 bp) (* 405 bq) (* 551 br) (* 617 bs) (* 565 bt) (* 445 bu) (* 574 bv) (* 340 bw) (* 460 bx) (* 430 by) (* 596 bz) (* 322 ca) (* 588 cb) (* 342 cc) (* 338 cd) (* 428 ce) (* 523 cf) (* 467 cg) (* 294 ch) (* 401 ci) (* 206 cj) (* 7 ck) (* 30 cl) (* 103 cm) (* 137 cn) (* 2260 co) (* 256 cp) (* 5 cq) (* 259 cr) (* 8 cs) (* 251 ct) (* 191 cu) (* 179 cv) (* 786 cw) (* 262 cx) (* 6 cy) (* 194 cz) (* 45 da) (* 112 db) (* 219 dc) (* 55 dd) (* 1654 de) (* 3046 df) (* 14 dg) (* 1130 dh) (* 897 di) (* 492 dj) (* 280 dk) (* 347 dl) (* 118 dm) (* 235 dn) (* 253 do) (* 215 dp) (* 16 dq) (* 30 dr) ) 3000))
(assert (>= (+ (* 64 aa) (* 33 ab) (* 20 ac) (* 103 ad) (* 38 ae) (* 51 af) (* 146 ag) (* 171 ah) (* 259 ai) (* 42 aj) (* 134 ak) (* 217 al) (* 250 am) (* 1 an) (* 33 ao) (* 183 ap) (* 158 aq) (* 216 ar) (* 121 _as) (* 124 at) (* 31 au) (* 62 av) (* 39 aw) (* 30 ax) (* 1 ay) (* 257 az) (* 123 ba) (* 143 bb) (* 75 bc) (* 137 bd) (* 122 be) (* 134 bf) (* 0 bg) (* 50 bh) (* 79 bi) (* 188 bj) (* 174 bk) (* 200 bl) (* 1 bm) (* 97 bn) (* 48 bo) (* 76 bp) (* 149 bq) (* 47 br) (* 140 bs) (* 223 bt) (* 39 bu) (* 223 bv) (* 124 bw) (* 130 bx) (* 37 by) (* 48 bz) (* 33 ca) (* 149 cb) (* 80 cc) (* 125 cd) (* 73 ce) (* 232 cf) (* 139 cg) (* 231 ch) (* 394 ci) (* 27 cj) (* 4 ck) (* 10 cl) (* 4 cm) (* 13 cn) (* 45 co) (* 33 cp) (* 23 cq) (* 12 cr) (* 2 cs) (* 10 ct) (* 134 cu) (* 121 cv) (* 31 cw) (* 10 cx) (* 4 cy) (* 5 cz) (* 2 da) (* 60 db) (* 44 dc) (* 5 dd) (* 43 de) (* 76 df) (* 5 dg) (* 22 dh) (* 18 di) (* 10 dj) (* 174 dk) (* 181 dl) (* 89 dm) (* 143 dn) (* 144 do) (* 136 dp) (* 3 dq) (* 3 dr) ) 738))
(assert (>= (+ (* 102 aa) (* 149 ab) (* 319 ac) (* 214 ad) (* 320 ae) (* 149 af) (* 274 ag) (* 211 ah) (* 596 ai) (* 171 aj) (* 300 ak) (* 334 al) (* 428 am) (* 1 an) (* 227 ao) (* 211 ap) (* 121 aq) (* 318 ar) (* 184 _as) (* 301 at) (* 222 au) (* 225 av) (* 319 aw) (* 109 ax) (* 2 ay) (* 273 az) (* 273 ba) (* 275 bb) (* 205 bc) (* 235 bd) (* 215 be) (* 0 bf) (* 1 bg) (* 172 bh) (* 372 bi) (* 535 bj) (* 499 bk) (* 245 bl) (* 0 bm) (* 143 bn) (* 588 bo) (* 246 bp) (* 332 bq) (* 273 br) (* 402 bs) (* 436 bt) (* 400 bu) (* 435 bv) (* 242 bw) (* 475 bx) (* 395 by) (* 583 bz) (* 167 ca) (* 392 cb) (* 328 cc) (* 273 cd) (* 265 ce) (* 422 cf) (* 312 cg) (* 296 ch) (* 461 ci) (* 80 cj) (* 4 ck) (* 26 cl) (* 8 cm) (* 16 cn) (* 497 co) (* 282 cp) (* 18 cq) (* 266 cr) (* 3 cs) (* 264 ct) (* 140 cu) (* 125 cv) (* 758 cw) (* 253 cx) (* 10 cy) (* 47 cz) (* 5 da) (* 0 db) (* 75 dc) (* 23 dd) (* 754 de) (* 1255 df) (* 11 dg) (* 249 dh) (* 198 di) (* 108 dj) (* 187 dk) (* 218 dl) (* 70 dm) (* 154 dn) (* 167 do) (* 151 dp) (* 7 dq) (* 9 dr) ) 600))
(assert (>= (+ (* 0.8 aa) (* 0.9 ab) (* 0.8 ac) (* 1.1 ad) (* 0.9 ae) (* 1.1 af) (* 2.1 ag) (* 1.3 ah) (* 5.2 ai) (* 1.9 aj) (* 2.1 ak) (* 1.9 al) (* 3.1 am) (* 0 an) (* 0.8 ao) (* 1.7 ap) (* 0.8 aq) (* 2 ar) (* 1.2 _as) (* 0.8 at) (* 0.7 au) (* 0.7 av) (* 0.9 aw) (* 1.2 ax) (* 0 ay) (* 6.2 az) (* 2.9 ba) (* 2.2 bb) (* 0.5 bc) (* 1.3 bd) (* 1.3 be) (* 3.3 bf) (* 0 bg) (* 1.1 bh) (* 2 bi) (* 3.1 bj) (* 2.5 bk) (* 2.3 bl) (* 0 bm) (* 1 bn) (* 1.4 bo) (* 1.8 bp) (* 2.8 bq) (* 3.2 br) (* 3.4 bs) (* 3.2 bt) (* 1.1 bu) (* 3.5 bv) (* 1.9 bw) (* 1.1 bx) (* 1 by) (* 1.3 bz) (* 1.9 ca) (* 3.8 cb) (* 0.6 cc) (* 2.1 cd) (* 1.7 ce) (* 3.2 cf) (* 2.2 cg) (* 1.1 ch) (* 2 ci) (* 1.1 cj) (* 0 ck) (* 0.1 cl) (* 0.1 cm) (* 0.2 cn) (* 2.6 co) (* 0.5 cp) (* 0 cq) (* 0.5 cr) (* 0 cs) (* 0.4 ct) (* 0.3 cu) (* 0 cv) (* 1.4 cw) (* 0.5 cx) (* 0 cy) (* 0.3 cz) (* 0.1 da) (* 1.4 db) (* 2.9 dc) (* 0.3 dd) (* 2.2 de) (* 4 df) (* 0.1 dg) (* 1.3 dh) (* 1 di) (* 0.6 dj) (* 0.5 dk) (* 1.5 dl) (* 0 dm) (* 0.2 dn) (* 0.4 do) (* 0.1 dp) (* 0.1 dq) (* 0.1 dr) ) 6.3))
(assert (>= (+ (* 8 aa) (* 10 ab) (* 11 ac) (* 60 ad) (* 10 ae) (* 11 af) (* 131 ag) (* 118 ah) (* 149 ai) (* 63 aj) (* 114 ak) (* 147 al) (* 127 am) (* 0 an) (* 25 ao) (* 118 ap) (* 48 aq) (* 118 ar) (* 61 _as) (* 62 at) (* 13 au) (* 13 av) (* 12 aw) (* 14 ax) (* 99 ay) (* 141 az) (* 141 ba) (* 74 bb) (* 28 bc) (* 118 bd) (* 61 be) (* 0 bf) (* 0 bg) (* 8 bh) (* 9 bi) (* 125 bj) (* 115 bk) (* 123 bl) (* 0 bm) (* 9 bn) (* 14 bo) (* 17 bp) (* 141 bq) (* 78 br) (* 129 bs) (* 161 bt) (* 35 bu) (* 137 bv) (* 71 bw) (* 72 bx) (* 22 by) (* 16 bz) (* 23 ca) (* 93 cb) (* 30 cc) (* 71 cd) (* 14 ce) (* 124 cf) (* 82 cg) (* 108 ch) (* 217 ci) (* 7 cj) (* 1 ck) (* 7 cl) (* 9 cm) (* 27 cn) (* 0 co) (* 7 cp) (* 3 cq) (* 10 cr) (* 6 cs) (* 4 ct) (* 255 cu) (* 42 cv) (* 69 cw) (* 23 cx) (* 3 cy) (* 0 cz) (* 3 da) (* 8 db) (* 4 dc) (* 1 dd) (* 46 de) (* 69 df) (* 1 dg) (* 0 dh) (* 0 di) (* 0 dj) (* 61 dk) (* 61 dl) (* 10 dm) (* 47 dn) (* 47 do) (* 47 dp) (* 5 dq) (* 0 dr) ) 625))
(assert (>= (+ (* 0.09 aa) (* 0.16 ab) (* 0.13 ac) (* 0.11 ad) (* 0.16 ae) (* 0.19 af) (* 0.13 ag) (* 0.13 ah) (* 0.31 ai) (* 0.17 aj) (* 0.24 ak) (* 0.18 al) (* 0.23 am) (* 0 an) (* 0.11 ao) (* 0.18 ap) (* 0.15 aq) (* 0.13 ar) (* 0.1 _as) (* 0.11 at) (* 0.12 au) (* 0.15 av) (* 0.16 aw) (* 0.1 ax) (* 0 ay) (* 0.25 az) (* 0.25 ba) (* 0.17 bb) (* 0.11 bc) (* 0.14 bd) (* 0.14 be) (* 0 bf) (* 0 bg) (* 0.26 bh) (* 0.3 bi) (* 0.32 bj) (* 0.23 bk) (* 0.28 bl) (* 0 bm) (* 0.1 bn) (* 0.26 bo) (* 0.32 bp) (* 0.16 bq) (* 0.21 br) (* 0.28 bs) (* 0.22 bt) (* 0.16 bu) (* 0.18 bv) (* 0.13 bw) (* 0.16 bx) (* 0.17 by) (* 0.26 bz) (* 0.12 ca) (* 0.22 cb) (* 0.17 cc) (* 0.16 cd) (* 0.39 ce) (* 0.19 cf) (* 0.25 cg) (* 0.2 ch) (* 0.14 ci) (* 0.1 cj) (* 0 ck) (* 0.04 cl) (* 0.02 cm) (* 0.03 cn) (* 0.61 co) (* 0.1 cp) (* 0 cq) (* 0.31 cr) (* 0.22 cs) (* 0.09 ct) (* 0.05 cu) (* 0.05 cv) (* 0.28 cw) (* 0.09 cx) (* 0.01 cy) (* 0.05 cz) (* 0.01 da) (* 0 db) (* 0.08 dc) (* 0.05 dd) (* 0.5 de) (* 0.9 df) (* 0.01 dg) (* 0.31 dh) (* 0.24 di) (* 0.13 dj) (* 0.07 dk) (* 0.09 dl) (* 0.03 dm) (* 0.07 dn) (* 0.07 do) (* 0.07 dp) (* 0.01 dq) (* 0.01 dr) ) 1.4))
(assert (>= (+ (* 0.06 aa) (* 0.16 ab) (* 0.09 ac) (* 0.14 ad) (* 0.12 ae) (* 0.19 af) (* 0.36 ag) (* 0.31 ah) (* 0.54 ai) (* 0.16 aj) (* 0.25 ak) (* 0.3 al) (* 0.38 am) (* 0 an) (* 0.09 ao) (* 0.37 ap) (* 0.17 aq) (* 0.28 ar) (* 0.16 _as) (* 0.16 at) (* 0.09 au) (* 0.1 av) (* 0.12 aw) (* 0.09 ax) (* 0 ay) (* 0.51 az) (* 0.51 ba) (* 0.24 bb) (* 0.09 bc) (* 0.31 bd) (* 0.18 be) (* 0 bf) (* 0 bg) (* 0.21 bh) (* 0.2 bi) (* 0.46 bj) (* 0.41 bk) (* 0.45 bl) (* 0 bm) (* 0.08 bn) (* 0.2 bo) (* 0.35 bp) (* 0.42 bq) (* 0.26 br) (* 0.35 bs) (* 0.4 bt) (* 0.14 bu) (* 0.39 bv) (* 0.22 bw) (* 0.21 bx) (* 0.14 by) (* 0.2 bz) (* 0.15 ca) (* 0.35 cb) (* 0.13 cc) (* 0.23 cd) (* 0.36 ce) (* 0.37 cf) (* 0.24 cg) (* 0.32 ch) (* 0.41 ci) (* 0.06 cj) (* 0.01 ck) (* 0.01 cl) (* 0.01 cm) (* 0.02 cn) (* 0.07 co) (* 0.09 cp) (* 0.01 cq) (* 0.09 cr) (* 0.01 cs) (* 0.08 ct) (* 0.24 cu) (* 0.2 cv) (* 0.31 cw) (* 0.1 cx) (* 0.01 cy) (* 0.01 cz) (* 0 da) (* 0 db) (* 0.03 dc) (* 0 dd) (* 0.24 de) (* 0.38 df) (* 0 dg) (* 0.03 dh) (* 0.03 di) (* 0.01 dj) (* 0.29 dk) (* 0.3 dl) (* 0.13 dm) (* 0.23 dn) (* 0.26 do) (* 0.23 dp) (* 0 dq) (* 0.01 dr) ) 1.6))
(assert (>= (+ (* 1 aa) (* 3.3 ab) (* 7.9 ac) (* 2.3 ad) (* 8.1 ae) (* 3.6 af) (* 2.6 ag) (* 1.2 ah) (* 10.7 ai) (* 3.9 aj) (* 4.8 ak) (* 4.3 al) (* 6.2 am) (* 0 an) (* 5 ao) (* 2.9 ap) (* 2.9 aq) (* 4.1 ar) (* 2.5 _as) (* 5 at) (* 5.3 au) (* 5.6 av) (* 8.2 aw) (* 2.5 ax) (* 0 ay) (* 3.9 az) (* 3.9 ba) (* 4.4 bb) (* 1.4 bc) (* 1.3 bd) (* 2.6 be) (* 0 bf) (* 0 bg) (* 4.3 bh) (* 4.2 bi) (* 4.2 bj) (* 2.6 bk) (* 5.4 bl) (* 0 bm) (* 1.3 bn) (* 15.8 bo) (* 6.6 bp) (* 4.1 bq) (* 6.6 br) (* 7.5 bs) (* 7 bt) (* 9.5 bu) (* 7.2 bv) (* 4.1 bw) (* 9.5 bx) (* 9.8 by) (* 15.7 bz) (* 4 ca) (* 7.5 cb) (* 2.1 cc) (* 4.1 cd) (* 7.3 ce) (* 6.4 cf) (* 4.9 cg) (* 3.6 ch) (* 4.1 ci) (* 1 cj) (* 0 ck) (* 0.1 cl) (* 0.3 cm) (* 0.2 cn) (* 12.5 co) (* 7.7 cp) (* 0.1 cq) (* 7.6 cr) (* 0 cs) (* 7.6 ct) (* 0.2 cu) (* 0.2 cv) (* 21.3 cw) (* 7.1 cx) (* 0 cy) (* 0.9 cz) (* 0.2 da) (* 0 db) (* 0.8 dc) (* 0.3 dd) (* 20.5 de) (* 33.9 df) (* 0.1 dg) (* 6.3 dh) (* 5 di) (* 2.7 dj) (* 0.3 dk) (* 0.6 dl) (* 0.1 dm) (* 0.4 dn) (* 0.4 do) (* 0.3 dp) (* 0.1 dq) (* 0.1 dr) ) 15))
(assert (>= (+ (* 1 aa) (* 1 ab) (* 1 ac) (* 6 ad) (* 1 ae) (* 1 af) (* 1 ag) (* 0 ah) (* 2 ai) (* 6 aj) (* 17 ak) (* 7 al) (* 2 am) (* 0 an) (* 1 ao) (* 0 ap) (* 0 aq) (* 1 ar) (* 1 _as) (* 1 at) (* 0 au) (* 0 av) (* 1 aw) (* 1 ax) (* 0 ay) (* 1 az) (* 1 ba) (* 2 bb) (* 0 bc) (* 6 bd) (* 7 be) (* 0 bf) (* 0 bg) (* 6 bh) (* 0 bi) (* 0 bj) (* 5 bk) (* 6 bl) (* 0 bm) (* 1 bn) (* 2 bo) (* 2 bp) (* 1 bq) (* 6 br) (* 17 bs) (* 7 bt) (* 1 bu) (* 1 bv) (* 1 bw) (* 1 bx) (* 0 by) (* 1 bz) (* 1 ca) (* 2 cb) (* 0 cc) (* 7 cd) (* 6 ce) (* 0 cf) (* 17 cg) (* 1 ch) (* 1 ci) (* 8 cj) (* 5 ck) (* 0 cl) (* 19 cm) (* 15 cn) (* 40 co) (* 0 cp) (* 0 cq) (* 0 cr) (* 0 cs) (* 0 ct) (* 0 cu) (* 0 cv) (* 3 cw) (* 1 cx) (* 0 cy) (* 1 cz) (* 1 da) (* 0 db) (* 0 dc) (* 0 dd) (* 22 de) (* 43 df) (* 0 dg) (* 20 dh) (* 16 di) (* 9 dj) (* 0 dk) (* 0 dl) (* 0 dm) (* 3 dn) (* 0 do) (* 0 dp) (* 0 dq) (* 0 dr) ) 100))
(assert (>= (+ (* 66 aa) (* 56 ab) (* 49 ac) (* 47 ad) (* 50 ae) (* 56 af) (* 248 ag) (* 231 ah) (* 187 ai) (* 49 aj) (* 73 ak) (* 74 al) (* 109 am) (* 0 an) (* 37 ao) (* 255 ap) (* 45 aq) (* 76 ar) (* 38 _as) (* 50 at) (* 35 au) (* 35 av) (* 49 aw) (* 26 ax) (* 18 ay) (* 478 az) (* 458 ba) (* 69 bb) (* 40 bc) (* 228 bd) (* 47 be) (* 21 bf) (* 0 bg) (* 54 bh) (* 30 bi) (* 254 bj) (* 227 bk) (* 294 bl) (* 0 bm) (* 126 bn) (* 93 bo) (* 105 bp) (* 274 bq) (* 93 br) (* 118 bs) (* 119 bt) (* 69 bu) (* 127 bv) (* 64 bw) (* 82 bx) (* 66 by) (* 92 bz) (* 52 ca) (* 121 cb) (* 68 cc) (* 73 cd) (* 103 ce) (* 113 cf) (* 68 cg) (* 79 ch) (* 99 ci) (* 0 cj) (* 0 ck) (* 7 cl) (* 0 cm) (* 0 cn) (* 23 co) (* 44 cp) (* 1 cq) (* 43 cr) (* 0 cs) (* 43 ct) (* 116 cu) (* 12 cv) (* 188 cw) (* 63 cx) (* 7 cy) (* 4 cz) (* 0 da) (* 11 db) (* 5 dc) (* 2 dd) (* 136 de) (* 210 df) (* 2 dg) (* 11 dh) (* 9 di) (* 5 dj) (* 17 dk) (* 17 dl) (* 4 dm) (* 14 dn) (* 14 do) (* 14 dp) (* 6 dq) (* 0 dr) ) 0))
(assert (>= (+ (* 2.9 aa) (* 0.8 ab) (* 1.9 ac) (* 0.9 ad) (* 2.8 ae) (* 1.7 af) (* 1.5 ag) (* 1.7 ah) (* 3.2 ai) (* 2.3 aj) (* 2.4 ak) (* 1.9 al) (* 3.2 am) (* 0.2 an) (* 2.2 ao) (* 1.7 ap) (* 1.7 aq) (* 1.7 ar) (* 1.5 _as) (* 2.2 at) (* 1.9 au) (* 2.5 av) (* 2.8 aw) (* 1.5 ax) (* 0 ay) (* 6.1 az) (* 3.2 ba) (* 2.6 bb) (* 2.1 bc) (* 1.1 bd) (* 1.7 be) (* 2.8 bf) (* 0 bg) (* 1.5 bh) (* 1.6 bi) (* 1.7 bj) (* 1.8 bk) (* 2 bl) (* 0 bm) (* 3.9 bn) (* 4 bo) (* 1.8 bp) (* 1.6 bq) (* 2.3 br) (* 2.5 bs) (* 2 bt) (* 2.9 bu) (* 1.8 bv) (* 1.6 bw) (* 2.9 bx) (* 2.5 by) (* 3.9 bz) (* 1.6 ca) (* 2.7 cb) (* 3 cc) (* 1.8 cd) (* 1.5 ce) (* 1.8 cf) (* 2.3 cg) (* 1.7 ch) (* 1.7 ci) (* 2.9 cj) (* 0 ck) (* 0.5 cl) (* 0.4 cm) (* 0.8 cn) (* 12 co) (* 1.1 cp) (* 0 cq) (* 1.2 cr) (* 0.1 cs) (* 1.1 ct) (* 0.2 cu) (* 0.3 cv) (* 2.6 cw) (* 0.9 cx) (* 0.1 cy) (* 1.5 cz) (* 0.3 da) (* 1.3 db) (* 2.3 dc) (* 1 dd) (* 7.7 de) (* 14.6 df) (* 0.3 dg) (* 6 dh) (* 4.8 di) (* 2.6 dj) (* 0.7 dk) (* 1.7 dl) (* 0.1 dm) (* 1 dn) (* 1.1 do) (* 0.7 dp) (* 0.1 dq) (* 0.1 dr) ) 21))
(assert (>= (+ (* 2.3 aa) (* 2.5 ab) (* 3.3 ac) (* 2.5 ad) (* 3.1 ae) (* 2.1 af) (* 2.1 ag) (* 1.6 ah) (* 6 ai) (* 2.1 aj) (* 2.7 ak) (* 2.9 al) (* 4.4 am) (* 0 an) (* 2.5 ao) (* 2 ap) (* 1.8 aq) (* 2.9 ar) (* 1.9 _as) (* 2.7 at) (* 2.2 au) (* 2.1 av) (* 2.9 aw) (* 1.4 ax) (* 0.1 ay) (* 4.2 az) (* 2.4 ba) (* 2.6 bb) (* 1.6 bc) (* 1.6 bd) (* 2.1 be) (* 1.8 bf) (* 0 bg) (* 2.3 bh) (* 2.5 bi) (* 3 bj) (* 2.6 bk) (* 3.4 bl) (* 0.6 bm) (* 3.3 bn) (* 5.3 bo) (* 3.3 bp) (* 2.4 bq) (* 2.5 br) (* 3.1 bs) (* 3.3 bt) (* 3.8 bu) (* 3.6 bv) (* 2.3 bw) (* 4 bx) (* 3.4 by) (* 4.5 bz) (* 1.8 ca) (* 3.3 cb) (* 2.1 cc) (* 2.5 cd) (* 2.9 ce) (* 3.6 cf) (* 3.4 cg) (* 3.2 ch) (* 3 ci) (* 0.2 cj) (* 0 ck) (* 0.6 cl) (* 0.5 cm) (* 0 cn) (* 2.1 co) (* 2 cp) (* 0.4 cq) (* 1.9 cr) (* 0.2 cs) (* 1.6 ct) (* 0.1 cu) (* 0.2 cv) (* 3.9 cw) (* 1.3 cx) (* 0.7 cy) (* 0.8 cz) (* 0.5 da) (* 0.8 db) (* 0.4 dc) (* 0.6 dd) (* 3.6 de) (* 6 df) (* 0.5 dg) (* 1.1 dh) (* 0.8 di) (* 0.5 dj) (* 0.4 dk) (* 0.7 dl) (* 0.1 dm) (* 0.3 dn) (* 0.3 do) (* 0.3 dp) (* 0.6 dq) (* 1 dr) ) 5))

;; objective
(minimize (+ (* 395 aa) (* 545 ab) (* 532 ac) (* 441 ad) (* 498 ae) (* 478 af) (* 387 ag) (* 311 ah) (* 1067 ai) (* 428 aj) (* 527 ak) (* 489 al) (* 776 am) (* 38 an) (* 389 ao) (* 475 ap) (* 395 aq) (* 457 ar) (* 307 _as) (* 431 at) (* 345 au) (* 364 av) (* 465 aw) (* 256 ax) (* 60 ay) (* 979 az) (* 659 ba) (* 525 bb) (* 323 bc) (* 292 bd) (* 374 be) (* 319 bf) (* 121 bg) (* 419 bh) (* 420 bi) (* 550 bj) (* 396 bk) (* 695 bl) (* 1 bm) (* 553 bn) (* 768 bo) (* 728 bp) (* 486 bq) (* 594 br) (* 693 bs) (* 655 bt) (* 542 bu) (* 655 bv) (* 406 bw) (* 584 bx) (* 498 by) (* 709 bz) (* 356 ca) (* 724 cb) (* 434 cc) (* 473 cd) (* 642 ce) (* 625 cf) (* 471 cg) (* 579 ch) (* 558 ci) (* 83 cj) (* 31 ck) (* 287 cl) (* 23 cm) (* 10 cn) (* 1034 co) (* 252 cp) (* 8 cq) (* 249 cr) (* 6 cs) (* 243 ct) (* 275 cu) (* 148 cv) (* 810 cw) (* 270 cx) (* 109 cy) (* 145 cz) (* 33 da) (* 161 db) (* 304 dc) (* 211 dd) (* 1057 de) (* 1844 df) (* 44 dg) (* 517 dh) (* 410 di) (* 225 dj) (* 235 dk) (* 337 dl) (* 59 dm) (* 257 dn) (* 295 do) (* 232 dp) (* 108 dq) (* 7 dr)))

;; solve the problem using the default solver
(check-sat)

;; print the value of the side salad variable at the optimum
(get-model)

実行してみましたが、1時間ほど待っても終わりません。元記事では 0.1 秒だったのに、なぜ？ 最強のソルバーを使ったら結果が出ないという、驚きの結果です。

でも Excel と違ってエラーは出さずに頑張ってくれています。

ちょっとずるいけどヒントを与える

ならばと、私の方も諦めないで3、少し記述の改良をしてみました。具体的には 3500 kcal を超えたらダメということを assert で伝えるようにしました。しかしこれでも出力できません。

Stack Overflow などで、私と同じように性能が出なくて困っている方の対処法を何件か見た結果、assert-soft という関数がしばしば使われていました。調べたところ、ソフト制約という、満たさなくても良いけれど、満たす方向で検討してほしい制約を与えられる機能だとわかりました。これを使って、できたらサラダは 282 個以上、塩・コショウは 18 個以上、バターパットは 7 個以上食べるような組み合わせを考えてほしいということを伝えます。

ちょっとずるいですが、ずるいのはほとんど答のようなヒントを教えてあげた私で、Z3 ちゃんは悪くありません。

この手のカンニングは Stack Overflow では広く行われているようです。たとえば 3500 kcal 以下というのも、100 kcal とかに設定変更すると一瞬で解なしと出ますので、じゃあ 200 kcal ではどうか、といったふうに徐々に正解に近づけていけば、そのうち最適解に到達するわけですね。各段階で、計算が終わればですが4。

assert-soft に関しても、人間なら「サラダ大事！ たぶん100個くらい食べないと！」と思うでしょうから、その感覚をソルバーに伝えてあげるのは良いことだと思います。

;; variables
(declare-const _as Int)
(declare-const aa Int)
(declare-const ab Int)
(declare-const ac Int)
(declare-const ad Int)
(declare-const ae Int)
(declare-const af Int)
(declare-const ag Int)
(declare-const ah Int)
(declare-const ai Int)
(declare-const aj Int)
(declare-const ak Int)
(declare-const al Int)
(declare-const am Int)
(declare-const an Int)
(declare-const ao Int)
(declare-const ap Int)
(declare-const aq Int)
(declare-const ar Int)
(declare-const at Int)
(declare-const au Int)
(declare-const av Int)
(declare-const aw Int)
(declare-const ax Int)
(declare-const ay Int)
(declare-const az Int)
(declare-const ba Int)
(declare-const bb Int)
(declare-const bc Int)
(declare-const bd Int)
(declare-const be Int)
(declare-const bf Int)
(declare-const bg Int)
(declare-const bh Int)
(declare-const bi Int)
(declare-const bj Int)
(declare-const bk Int)
(declare-const bl Int)
(declare-const bm Int)
(declare-const bn Int)
(declare-const bo Int)
(declare-const bp Int)
(declare-const bq Int)
(declare-const br Int)
(declare-const bs Int)
(declare-const bt Int)
(declare-const bu Int)
(declare-const bv Int)
(declare-const bw Int)
(declare-const bx Int)
(declare-const by Int)
(declare-const bz Int)
(declare-const ca Int)
(declare-const cb Int)
(declare-const cc Int)
(declare-const cd Int)
(declare-const ce Int)
(declare-const cf Int)
(declare-const cg Int)
(declare-const ch Int)
(declare-const ci Int)
(declare-const cj Int)
(declare-const ck Int)
(declare-const cl Int)
(declare-const cm Int)
(declare-const cn Int)
(declare-const co Int)
(declare-const cp Int)
(declare-const cq Int)
(declare-const cr Int)
(declare-const cs Int)
(declare-const ct Int)
(declare-const cu Int)
(declare-const cv Int)
(declare-const cw Int)
(declare-const cx Int)
(declare-const cy Int)
(declare-const cz Int)
(declare-const da Int)
(declare-const db Int)
(declare-const dc Int)
(declare-const dd Int)
(declare-const de Int)
(declare-const df Int)
(declare-const dg Int)
(declare-const dh Int)
(declare-const di Int)
(declare-const dj Int)
(declare-const dk Int)
(declare-const dl Int)
(declare-const dm Int)
(declare-const dn Int)
(declare-const do Int)
(declare-const dp Int)
(declare-const dq Int)
(declare-const dr Int)
(assert (and (>= _as 0) (>= aa 0) (>= ab 0) (>= ac 0) (>= ad 0) (>= ae 0) (>= af 0) (>= ag 0) (>= ah 0) (>= ai 0) (>= aj 0) (>= ak 0) (>= al 0) (>= am 0) (>= an 0) (>= ao 0) (>= ap 0) (>= aq 0) (>= ar 0) (>= at 0) (>= au 0) (>= av 0) (>= aw 0) (>= ax 0) (>= ay 0) (>= az 0) (>= ba 0) (>= bb 0) (>= bc 0) (>= bd 0) (>= be 0) (>= bf 0) (>= bg 0) (>= bh 0) (>= bi 0) (>= bj 0) (>= bk 0) (>= bl 0) (>= bm 0) (>= bn 0) (>= bo 0) (>= bp 0) (>= bq 0) (>= br 0) (>= bs 0) (>= bt 0) (>= bu 0) (>= bv 0) (>= bw 0) (>= bx 0) (>= by 0) (>= bz 0) (>= ca 0) (>= cb 0) (>= cc 0) (>= cd 0) (>= ce 0) (>= cf 0) (>= cg 0) (>= ch 0) (>= ci 0) (>= cj 0) (>= ck 0) (>= cl 0) (>= cm 0) (>= cn 0) (>= co 0) (>= cp 0) (>= cq 0) (>= cr 0) (>= cs 0) (>= ct 0) (>= cu 0) (>= cv 0) (>= cw 0) (>= cx 0) (>= cy 0) (>= cz 0) (>= da 0) (>= db 0) (>= dc 0) (>= dd 0) (>= de 0) (>= df 0) (>= dg 0) (>= dh 0) (>= di 0) (>= dj 0) (>= dk 0) (>= dl 0) (>= dm 0) (>= dn 0) (>= do 0) (>= dp 0) (>= dq 0) (>= dr 0)))

;; constraints
(assert (>= (+ (* 12.5 aa) (* 14.5 ab) (* 19 ac) (* 16.7 ad) (* 20.2 ae) (* 15.5 af) (* 22.3 ag) (* 19.2 ah) (* 61.9 ai) (* 19.9 aj) (* 26.5 ak) (* 27.3 al) (* 39.5 am) (* 0 an) (* 14.2 ao) (* 21.5 ap) (* 15 aq) (* 26.5 ar) (* 15.8 _as) (* 17.1 at) (* 14 au) (* 15.2 av) (* 20 aw) (* 12.8 ax) (* 0 ay) (* 34.1 az) (* 26.2 ba) (* 26 bb) (* 14.4 bc) (* 15.9 bd) (* 17.7 be) (* 8 bf) (* 0 bg) (* 17.2 bh) (* 10.4 bi) (* 20.3 bj) (* 15.7 bk) (* 29.7 bl) (* 0 bm) (* 19.4 bn) (* 35.3 bo) (* 25.8 bp) (* 30 bq) (* 33.3 br) (* 39.8 bs) (* 40.6 bt) (* 23.2 bu) (* 42 bv) (* 23.5 bw) (* 26.1 bx) (* 23 by) (* 34.8 bz) (* 20.6 ca) (* 41.4 cb) (* 22.7 cc) (* 25.5 cd) (* 27.2 ce) (* 39 cf) (* 26.7 cg) (* 21.4 ch) (* 32.4 ci) (* 5.2 cj) (* 0.2 ck) (* 3 cl) (* 0.4 cm) (* 0.5 cn) (* 13.4 co) (* 15.3 cp) (* 0.5 cq) (* 15 cr) (* 0.2 cs) (* 14.8 ct) (* 5 cu) (* 3.8 cv) (* 47.3 cw) (* 15.8 cx) (* 0.3 cy) (* 1.2 cz) (* 0.2 da) (* 3.8 db) (* 3.7 dc) (* 1.9 dd) (* 38.2 de) (* 60.6 df) (* 0.4 dg) (* 6.7 dh) (* 5.3 di) (* 2.9 dj) (* 5.9 dk) (* 8 dl) (* 3.2 dm) (* 5.4 dn) (* 5.9 do) (* 5.3 dp) (* 0.4 dq) (* 0.4 dr) ) 39))
(assert (>= (+ (* 17.4 aa) (* 29.4 ab) (* 21.1 ac) (* 20 ad) (* 23.2 ae) (* 30.2 af) (* 18.9 ag) (* 13.5 ah) (* 65.5 ai) (* 21.7 aj) (* 30.7 ak) (* 26.6 al) (* 43.1 am) (* 0 an) (* 20.2 ao) (* 30.6 ap) (* 25.1 aq) (* 25 ar) (* 13.4 _as) (* 23 at) (* 15.5 au) (* 17.3 av) (* 21.9 aw) (* 9.4 ax) (* 6.7 ay) (* 51.3 az) (* 42.7 ba) (* 28.3 bb) (* 13.9 bc) (* 13.3 bd) (* 20.8 be) (* 8.6 bf) (* 0 bg) (* 23.7 bh) (* 23.8 bi) (* 33.2 bj) (* 18.1 bk) (* 49.7 bl) (* 0 bm) (* 25.5 bn) (* 36.1 bo) (* 50 bp) (* 26.5 bq) (* 34.2 br) (* 43.2 bs) (* 39.1 bt) (* 28.7 bu) (* 40.1 bv) (* 21 bw) (* 31.6 bx) (* 24 by) (* 34.7 bz) (* 16.9 ca) (* 43.4 cb) (* 18.6 cc) (* 28.4 cd) (* 43.5 ce) (* 36.2 cf) (* 23.7 cg) (* 38.3 ch) (* 33.1 ci) (* 3 cj) (* 1.5 ck) (* 18 cl) (* 0 cm) (* 0.1 cn) (* 51.8 co) (* 13.1 cp) (* 0.2 cq) (* 12.9 cr) (* 0 cs) (* 12.8 ct) (* 18.9 cu) (* 3.9 cv) (* 51.6 cw) (* 17.2 cx) (* 11.2 cy) (* 9.6 cz) (* 0.1 da) (* 4.4 db) (* 18.1 dc) (* 10.7 dd) (* 60.3 de) (* 103.4 df) (* 2.3 dg) (* 25.9 dh) (* 20.6 di) (* 11.3 dj) (* 7 dk) (* 10.6 dl) (* 0.8 dm) (* 5.5 dn) (* 10.7 do) (* 5.5 dp) (* 10.9 dq) (* 0 dr) ) 75))
(assert (>= (+ (* 47.7 aa) (* 55.8 ab) (* 66.6 ac) (* 48.4 ad) (* 52.4 ae) (* 36.4 af) (* 31 ag) (* 27.1 ah) (* 57.5 ai) (* 38.9 aj) (* 36.8 ak) (* 35.5 al) (* 57.5 am) (* 9.5 an) (* 38.1 ao) (* 27.3 ap) (* 27.2 aq) (* 31.4 ar) (* 30.8 _as) (* 39.2 at) (* 37.7 au) (* 37 av) (* 47.3 aw) (* 30.3 ax) (* 0 ay) (* 92.9 az) (* 40.2 ba) (* 41.8 bb) (* 35.8 bc) (* 26.4 bd) (* 29.1 be) (* 52.7 bf) (* 30.2 bg) (* 34.3 bh) (* 41.9 bi) (* 42.4 bj) (* 42.4 bk) (* 31.2 bl) (* 0.1 bm) (* 62.8 bn) (* 76 bo) (* 44.1 bp) (* 31 bq) (* 38.9 br) (* 36.8 bs) (* 35.5 bt) (* 48 bu) (* 31.4 bv) (* 30.8 bw) (* 49.1 bx) (* 47.6 by) (* 64.4 bz) (* 30.3 ca) (* 41.8 cb) (* 45 cc) (* 29.1 cd) (* 35.5 ce) (* 36.3 cf) (* 38.2 cg) (* 37.6 ch) (* 32.7 ci) (* 9.6 cj) (* 4.3 ck) (* 28.3 cl) (* 5.6 cm) (* 2.3 cn) (* 128.5 co) (* 18.2 cp) (* 1.1 cq) (* 18.3 cr) (* 1.2 cs) (* 17.2 ct) (* 21.1 cu) (* 24.7 cv) (* 39.2 cw) (* 13.1 cx) (* 1.6 cy) (* 13.3 cz) (* 7.7 da) (* 26.4 db) (* 31.5 dc) (* 26.8 dd) (* 90.4 de) (* 167.7 df) (* 5.2 dg) (* 64.3 dh) (* 51 di) (* 28 dj) (* 37.7 dk) (* 53.4 dl) (* 9.7 dm) (* 46.8 dn) (* 44.1 do) (* 40.6 dp) (* 2 dq) (* 1.2 dr) ) 675))
(assert (>= (+ (* 919 aa) (* 986 ab) (* 1296 ac) (* 994 ad) (* 1216 ae) (* 829 af) (* 813 ag) (* 649 ah) (* 2326 ai) (* 816 aj) (* 1052 ak) (* 1129 al) (* 1714 am) (* 4 an) (* 996 ao) (* 789 ap) (* 722 aq) (* 1132 ar) (* 747 _as) (* 1060 at) (* 850 au) (* 813 av) (* 1139 aw) (* 542 ax) (* 36 ay) (* 1673 az) (* 962 ba) (* 1007 bb) (* 644 bc) (* 636 bd) (* 837 be) (* 711 bf) (* 1 bg) (* 890 bh) (* 971 bi) (* 1193 bj) (* 1030 bk) (* 1358 bl) (* 254 bm) (* 1309 bn) (* 2082 bo) (* 1308 bp) (* 965 bq) (* 987 br) (* 1223 bs) (* 1300 bt) (* 1501 bu) (* 1435 bv) (* 898 bw) (* 1565 bx) (* 1355 by) (* 1778 bz) (* 693 ca) (* 1310 cb) (* 816 cc) (* 989 cd) (* 1142 ce) (* 1428 cf) (* 1340 cg) (* 1245 ch) (* 1554 ci) (* 84 cj) (* 2 ck) (* 222 cl) (* 210 cm) (* 1 cn) (* 830 co) (* 791 cp) (* 152 cq) (* 730 cr) (* 91 cs) (* 639 ct) (* 55 cu) (* 83 cv) (* 1517 cw) (* 506 cx) (* 283 cy) (* 307 cz) (* 182 da) (* 318 db) (* 154 dc) (* 217 dd) (* 1426 de) (* 2346 df) (* 182 dg) (* 415 dh) (* 329 di) (* 181 dj) (* 155 dk) (* 268 dl) (* 37 dm) (* 135 dn) (* 118 do) (* 118 dp) (* 222 dq) (* 384 dr) ) 5000))
(assert (>= (+ (* 119 aa) (* 237 ab) (* 328 ac) (* 212 ad) (* 343 ae) (* 255 af) (* 297 ag) (* 183 ah) (* 860 ai) (* 366 aj) (* 432 ak) (* 379 al) (* 536 am) (* 7 an) (* 262 ao) (* 235 ap) (* 170 aq) (* 358 ar) (* 232 _as) (* 277 at) (* 246 au) (* 258 av) (* 345 aw) (* 214 ax) (* 0 ay) (* 730 az) (* 477 ba) (* 372 bb) (* 198 bc) (* 148 bd) (* 230 be) (* 254 bf) (* 0 bg) (* 266 bh) (* 167 bi) (* 256 bj) (* 172 bk) (* 415 bl) (* 2 bm) (* 138 bn) (* 610 bo) (* 433 bp) (* 405 bq) (* 551 br) (* 617 bs) (* 565 bt) (* 445 bu) (* 574 bv) (* 340 bw) (* 460 bx) (* 430 by) (* 596 bz) (* 322 ca) (* 588 cb) (* 342 cc) (* 338 cd) (* 428 ce) (* 523 cf) (* 467 cg) (* 294 ch) (* 401 ci) (* 206 cj) (* 7 ck) (* 30 cl) (* 103 cm) (* 137 cn) (* 2260 co) (* 256 cp) (* 5 cq) (* 259 cr) (* 8 cs) (* 251 ct) (* 191 cu) (* 179 cv) (* 786 cw) (* 262 cx) (* 6 cy) (* 194 cz) (* 45 da) (* 112 db) (* 219 dc) (* 55 dd) (* 1654 de) (* 3046 df) (* 14 dg) (* 1130 dh) (* 897 di) (* 492 dj) (* 280 dk) (* 347 dl) (* 118 dm) (* 235 dn) (* 253 do) (* 215 dp) (* 16 dq) (* 30 dr) ) 3000))
(assert (>= (+ (* 64 aa) (* 33 ab) (* 20 ac) (* 103 ad) (* 38 ae) (* 51 af) (* 146 ag) (* 171 ah) (* 259 ai) (* 42 aj) (* 134 ak) (* 217 al) (* 250 am) (* 1 an) (* 33 ao) (* 183 ap) (* 158 aq) (* 216 ar) (* 121 _as) (* 124 at) (* 31 au) (* 62 av) (* 39 aw) (* 30 ax) (* 1 ay) (* 257 az) (* 123 ba) (* 143 bb) (* 75 bc) (* 137 bd) (* 122 be) (* 134 bf) (* 0 bg) (* 50 bh) (* 79 bi) (* 188 bj) (* 174 bk) (* 200 bl) (* 1 bm) (* 97 bn) (* 48 bo) (* 76 bp) (* 149 bq) (* 47 br) (* 140 bs) (* 223 bt) (* 39 bu) (* 223 bv) (* 124 bw) (* 130 bx) (* 37 by) (* 48 bz) (* 33 ca) (* 149 cb) (* 80 cc) (* 125 cd) (* 73 ce) (* 232 cf) (* 139 cg) (* 231 ch) (* 394 ci) (* 27 cj) (* 4 ck) (* 10 cl) (* 4 cm) (* 13 cn) (* 45 co) (* 33 cp) (* 23 cq) (* 12 cr) (* 2 cs) (* 10 ct) (* 134 cu) (* 121 cv) (* 31 cw) (* 10 cx) (* 4 cy) (* 5 cz) (* 2 da) (* 60 db) (* 44 dc) (* 5 dd) (* 43 de) (* 76 df) (* 5 dg) (* 22 dh) (* 18 di) (* 10 dj) (* 174 dk) (* 181 dl) (* 89 dm) (* 143 dn) (* 144 do) (* 136 dp) (* 3 dq) (* 3 dr) ) 738))
(assert (>= (+ (* 102 aa) (* 149 ab) (* 319 ac) (* 214 ad) (* 320 ae) (* 149 af) (* 274 ag) (* 211 ah) (* 596 ai) (* 171 aj) (* 300 ak) (* 334 al) (* 428 am) (* 1 an) (* 227 ao) (* 211 ap) (* 121 aq) (* 318 ar) (* 184 _as) (* 301 at) (* 222 au) (* 225 av) (* 319 aw) (* 109 ax) (* 2 ay) (* 273 az) (* 273 ba) (* 275 bb) (* 205 bc) (* 235 bd) (* 215 be) (* 0 bf) (* 1 bg) (* 172 bh) (* 372 bi) (* 535 bj) (* 499 bk) (* 245 bl) (* 0 bm) (* 143 bn) (* 588 bo) (* 246 bp) (* 332 bq) (* 273 br) (* 402 bs) (* 436 bt) (* 400 bu) (* 435 bv) (* 242 bw) (* 475 bx) (* 395 by) (* 583 bz) (* 167 ca) (* 392 cb) (* 328 cc) (* 273 cd) (* 265 ce) (* 422 cf) (* 312 cg) (* 296 ch) (* 461 ci) (* 80 cj) (* 4 ck) (* 26 cl) (* 8 cm) (* 16 cn) (* 497 co) (* 282 cp) (* 18 cq) (* 266 cr) (* 3 cs) (* 264 ct) (* 140 cu) (* 125 cv) (* 758 cw) (* 253 cx) (* 10 cy) (* 47 cz) (* 5 da) (* 0 db) (* 75 dc) (* 23 dd) (* 754 de) (* 1255 df) (* 11 dg) (* 249 dh) (* 198 di) (* 108 dj) (* 187 dk) (* 218 dl) (* 70 dm) (* 154 dn) (* 167 do) (* 151 dp) (* 7 dq) (* 9 dr) ) 600))
(assert (>= (+ (* 0.8 aa) (* 0.9 ab) (* 0.8 ac) (* 1.1 ad) (* 0.9 ae) (* 1.1 af) (* 2.1 ag) (* 1.3 ah) (* 5.2 ai) (* 1.9 aj) (* 2.1 ak) (* 1.9 al) (* 3.1 am) (* 0 an) (* 0.8 ao) (* 1.7 ap) (* 0.8 aq) (* 2 ar) (* 1.2 _as) (* 0.8 at) (* 0.7 au) (* 0.7 av) (* 0.9 aw) (* 1.2 ax) (* 0 ay) (* 6.2 az) (* 2.9 ba) (* 2.2 bb) (* 0.5 bc) (* 1.3 bd) (* 1.3 be) (* 3.3 bf) (* 0 bg) (* 1.1 bh) (* 2 bi) (* 3.1 bj) (* 2.5 bk) (* 2.3 bl) (* 0 bm) (* 1 bn) (* 1.4 bo) (* 1.8 bp) (* 2.8 bq) (* 3.2 br) (* 3.4 bs) (* 3.2 bt) (* 1.1 bu) (* 3.5 bv) (* 1.9 bw) (* 1.1 bx) (* 1 by) (* 1.3 bz) (* 1.9 ca) (* 3.8 cb) (* 0.6 cc) (* 2.1 cd) (* 1.7 ce) (* 3.2 cf) (* 2.2 cg) (* 1.1 ch) (* 2 ci) (* 1.1 cj) (* 0 ck) (* 0.1 cl) (* 0.1 cm) (* 0.2 cn) (* 2.6 co) (* 0.5 cp) (* 0 cq) (* 0.5 cr) (* 0 cs) (* 0.4 ct) (* 0.3 cu) (* 0 cv) (* 1.4 cw) (* 0.5 cx) (* 0 cy) (* 0.3 cz) (* 0.1 da) (* 1.4 db) (* 2.9 dc) (* 0.3 dd) (* 2.2 de) (* 4 df) (* 0.1 dg) (* 1.3 dh) (* 1 di) (* 0.6 dj) (* 0.5 dk) (* 1.5 dl) (* 0 dm) (* 0.2 dn) (* 0.4 do) (* 0.1 dp) (* 0.1 dq) (* 0.1 dr) ) 6.3))
(assert (>= (+ (* 8 aa) (* 10 ab) (* 11 ac) (* 60 ad) (* 10 ae) (* 11 af) (* 131 ag) (* 118 ah) (* 149 ai) (* 63 aj) (* 114 ak) (* 147 al) (* 127 am) (* 0 an) (* 25 ao) (* 118 ap) (* 48 aq) (* 118 ar) (* 61 _as) (* 62 at) (* 13 au) (* 13 av) (* 12 aw) (* 14 ax) (* 99 ay) (* 141 az) (* 141 ba) (* 74 bb) (* 28 bc) (* 118 bd) (* 61 be) (* 0 bf) (* 0 bg) (* 8 bh) (* 9 bi) (* 125 bj) (* 115 bk) (* 123 bl) (* 0 bm) (* 9 bn) (* 14 bo) (* 17 bp) (* 141 bq) (* 78 br) (* 129 bs) (* 161 bt) (* 35 bu) (* 137 bv) (* 71 bw) (* 72 bx) (* 22 by) (* 16 bz) (* 23 ca) (* 93 cb) (* 30 cc) (* 71 cd) (* 14 ce) (* 124 cf) (* 82 cg) (* 108 ch) (* 217 ci) (* 7 cj) (* 1 ck) (* 7 cl) (* 9 cm) (* 27 cn) (* 0 co) (* 7 cp) (* 3 cq) (* 10 cr) (* 6 cs) (* 4 ct) (* 255 cu) (* 42 cv) (* 69 cw) (* 23 cx) (* 3 cy) (* 0 cz) (* 3 da) (* 8 db) (* 4 dc) (* 1 dd) (* 46 de) (* 69 df) (* 1 dg) (* 0 dh) (* 0 di) (* 0 dj) (* 61 dk) (* 61 dl) (* 10 dm) (* 47 dn) (* 47 do) (* 47 dp) (* 5 dq) (* 0 dr) ) 625))
(assert (>= (+ (* 0.09 aa) (* 0.16 ab) (* 0.13 ac) (* 0.11 ad) (* 0.16 ae) (* 0.19 af) (* 0.13 ag) (* 0.13 ah) (* 0.31 ai) (* 0.17 aj) (* 0.24 ak) (* 0.18 al) (* 0.23 am) (* 0 an) (* 0.11 ao) (* 0.18 ap) (* 0.15 aq) (* 0.13 ar) (* 0.1 _as) (* 0.11 at) (* 0.12 au) (* 0.15 av) (* 0.16 aw) (* 0.1 ax) (* 0 ay) (* 0.25 az) (* 0.25 ba) (* 0.17 bb) (* 0.11 bc) (* 0.14 bd) (* 0.14 be) (* 0 bf) (* 0 bg) (* 0.26 bh) (* 0.3 bi) (* 0.32 bj) (* 0.23 bk) (* 0.28 bl) (* 0 bm) (* 0.1 bn) (* 0.26 bo) (* 0.32 bp) (* 0.16 bq) (* 0.21 br) (* 0.28 bs) (* 0.22 bt) (* 0.16 bu) (* 0.18 bv) (* 0.13 bw) (* 0.16 bx) (* 0.17 by) (* 0.26 bz) (* 0.12 ca) (* 0.22 cb) (* 0.17 cc) (* 0.16 cd) (* 0.39 ce) (* 0.19 cf) (* 0.25 cg) (* 0.2 ch) (* 0.14 ci) (* 0.1 cj) (* 0 ck) (* 0.04 cl) (* 0.02 cm) (* 0.03 cn) (* 0.61 co) (* 0.1 cp) (* 0 cq) (* 0.31 cr) (* 0.22 cs) (* 0.09 ct) (* 0.05 cu) (* 0.05 cv) (* 0.28 cw) (* 0.09 cx) (* 0.01 cy) (* 0.05 cz) (* 0.01 da) (* 0 db) (* 0.08 dc) (* 0.05 dd) (* 0.5 de) (* 0.9 df) (* 0.01 dg) (* 0.31 dh) (* 0.24 di) (* 0.13 dj) (* 0.07 dk) (* 0.09 dl) (* 0.03 dm) (* 0.07 dn) (* 0.07 do) (* 0.07 dp) (* 0.01 dq) (* 0.01 dr) ) 1.4))
(assert (>= (+ (* 0.06 aa) (* 0.16 ab) (* 0.09 ac) (* 0.14 ad) (* 0.12 ae) (* 0.19 af) (* 0.36 ag) (* 0.31 ah) (* 0.54 ai) (* 0.16 aj) (* 0.25 ak) (* 0.3 al) (* 0.38 am) (* 0 an) (* 0.09 ao) (* 0.37 ap) (* 0.17 aq) (* 0.28 ar) (* 0.16 _as) (* 0.16 at) (* 0.09 au) (* 0.1 av) (* 0.12 aw) (* 0.09 ax) (* 0 ay) (* 0.51 az) (* 0.51 ba) (* 0.24 bb) (* 0.09 bc) (* 0.31 bd) (* 0.18 be) (* 0 bf) (* 0 bg) (* 0.21 bh) (* 0.2 bi) (* 0.46 bj) (* 0.41 bk) (* 0.45 bl) (* 0 bm) (* 0.08 bn) (* 0.2 bo) (* 0.35 bp) (* 0.42 bq) (* 0.26 br) (* 0.35 bs) (* 0.4 bt) (* 0.14 bu) (* 0.39 bv) (* 0.22 bw) (* 0.21 bx) (* 0.14 by) (* 0.2 bz) (* 0.15 ca) (* 0.35 cb) (* 0.13 cc) (* 0.23 cd) (* 0.36 ce) (* 0.37 cf) (* 0.24 cg) (* 0.32 ch) (* 0.41 ci) (* 0.06 cj) (* 0.01 ck) (* 0.01 cl) (* 0.01 cm) (* 0.02 cn) (* 0.07 co) (* 0.09 cp) (* 0.01 cq) (* 0.09 cr) (* 0.01 cs) (* 0.08 ct) (* 0.24 cu) (* 0.2 cv) (* 0.31 cw) (* 0.1 cx) (* 0.01 cy) (* 0.01 cz) (* 0 da) (* 0 db) (* 0.03 dc) (* 0 dd) (* 0.24 de) (* 0.38 df) (* 0 dg) (* 0.03 dh) (* 0.03 di) (* 0.01 dj) (* 0.29 dk) (* 0.3 dl) (* 0.13 dm) (* 0.23 dn) (* 0.26 do) (* 0.23 dp) (* 0 dq) (* 0.01 dr) ) 1.6))
(assert (>= (+ (* 1 aa) (* 3.3 ab) (* 7.9 ac) (* 2.3 ad) (* 8.1 ae) (* 3.6 af) (* 2.6 ag) (* 1.2 ah) (* 10.7 ai) (* 3.9 aj) (* 4.8 ak) (* 4.3 al) (* 6.2 am) (* 0 an) (* 5 ao) (* 2.9 ap) (* 2.9 aq) (* 4.1 ar) (* 2.5 _as) (* 5 at) (* 5.3 au) (* 5.6 av) (* 8.2 aw) (* 2.5 ax) (* 0 ay) (* 3.9 az) (* 3.9 ba) (* 4.4 bb) (* 1.4 bc) (* 1.3 bd) (* 2.6 be) (* 0 bf) (* 0 bg) (* 4.3 bh) (* 4.2 bi) (* 4.2 bj) (* 2.6 bk) (* 5.4 bl) (* 0 bm) (* 1.3 bn) (* 15.8 bo) (* 6.6 bp) (* 4.1 bq) (* 6.6 br) (* 7.5 bs) (* 7 bt) (* 9.5 bu) (* 7.2 bv) (* 4.1 bw) (* 9.5 bx) (* 9.8 by) (* 15.7 bz) (* 4 ca) (* 7.5 cb) (* 2.1 cc) (* 4.1 cd) (* 7.3 ce) (* 6.4 cf) (* 4.9 cg) (* 3.6 ch) (* 4.1 ci) (* 1 cj) (* 0 ck) (* 0.1 cl) (* 0.3 cm) (* 0.2 cn) (* 12.5 co) (* 7.7 cp) (* 0.1 cq) (* 7.6 cr) (* 0 cs) (* 7.6 ct) (* 0.2 cu) (* 0.2 cv) (* 21.3 cw) (* 7.1 cx) (* 0 cy) (* 0.9 cz) (* 0.2 da) (* 0 db) (* 0.8 dc) (* 0.3 dd) (* 20.5 de) (* 33.9 df) (* 0.1 dg) (* 6.3 dh) (* 5 di) (* 2.7 dj) (* 0.3 dk) (* 0.6 dl) (* 0.1 dm) (* 0.4 dn) (* 0.4 do) (* 0.3 dp) (* 0.1 dq) (* 0.1 dr) ) 15))
(assert (>= (+ (* 1 aa) (* 1 ab) (* 1 ac) (* 6 ad) (* 1 ae) (* 1 af) (* 1 ag) (* 0 ah) (* 2 ai) (* 6 aj) (* 17 ak) (* 7 al) (* 2 am) (* 0 an) (* 1 ao) (* 0 ap) (* 0 aq) (* 1 ar) (* 1 _as) (* 1 at) (* 0 au) (* 0 av) (* 1 aw) (* 1 ax) (* 0 ay) (* 1 az) (* 1 ba) (* 2 bb) (* 0 bc) (* 6 bd) (* 7 be) (* 0 bf) (* 0 bg) (* 6 bh) (* 0 bi) (* 0 bj) (* 5 bk) (* 6 bl) (* 0 bm) (* 1 bn) (* 2 bo) (* 2 bp) (* 1 bq) (* 6 br) (* 17 bs) (* 7 bt) (* 1 bu) (* 1 bv) (* 1 bw) (* 1 bx) (* 0 by) (* 1 bz) (* 1 ca) (* 2 cb) (* 0 cc) (* 7 cd) (* 6 ce) (* 0 cf) (* 17 cg) (* 1 ch) (* 1 ci) (* 8 cj) (* 5 ck) (* 0 cl) (* 19 cm) (* 15 cn) (* 40 co) (* 0 cp) (* 0 cq) (* 0 cr) (* 0 cs) (* 0 ct) (* 0 cu) (* 0 cv) (* 3 cw) (* 1 cx) (* 0 cy) (* 1 cz) (* 1 da) (* 0 db) (* 0 dc) (* 0 dd) (* 22 de) (* 43 df) (* 0 dg) (* 20 dh) (* 16 di) (* 9 dj) (* 0 dk) (* 0 dl) (* 0 dm) (* 3 dn) (* 0 do) (* 0 dp) (* 0 dq) (* 0 dr) ) 100))
(assert (>= (+ (* 66 aa) (* 56 ab) (* 49 ac) (* 47 ad) (* 50 ae) (* 56 af) (* 248 ag) (* 231 ah) (* 187 ai) (* 49 aj) (* 73 ak) (* 74 al) (* 109 am) (* 0 an) (* 37 ao) (* 255 ap) (* 45 aq) (* 76 ar) (* 38 _as) (* 50 at) (* 35 au) (* 35 av) (* 49 aw) (* 26 ax) (* 18 ay) (* 478 az) (* 458 ba) (* 69 bb) (* 40 bc) (* 228 bd) (* 47 be) (* 21 bf) (* 0 bg) (* 54 bh) (* 30 bi) (* 254 bj) (* 227 bk) (* 294 bl) (* 0 bm) (* 126 bn) (* 93 bo) (* 105 bp) (* 274 bq) (* 93 br) (* 118 bs) (* 119 bt) (* 69 bu) (* 127 bv) (* 64 bw) (* 82 bx) (* 66 by) (* 92 bz) (* 52 ca) (* 121 cb) (* 68 cc) (* 73 cd) (* 103 ce) (* 113 cf) (* 68 cg) (* 79 ch) (* 99 ci) (* 0 cj) (* 0 ck) (* 7 cl) (* 0 cm) (* 0 cn) (* 23 co) (* 44 cp) (* 1 cq) (* 43 cr) (* 0 cs) (* 43 ct) (* 116 cu) (* 12 cv) (* 188 cw) (* 63 cx) (* 7 cy) (* 4 cz) (* 0 da) (* 11 db) (* 5 dc) (* 2 dd) (* 136 de) (* 210 df) (* 2 dg) (* 11 dh) (* 9 di) (* 5 dj) (* 17 dk) (* 17 dl) (* 4 dm) (* 14 dn) (* 14 do) (* 14 dp) (* 6 dq) (* 0 dr) ) 0))
(assert (>= (+ (* 2.9 aa) (* 0.8 ab) (* 1.9 ac) (* 0.9 ad) (* 2.8 ae) (* 1.7 af) (* 1.5 ag) (* 1.7 ah) (* 3.2 ai) (* 2.3 aj) (* 2.4 ak) (* 1.9 al) (* 3.2 am) (* 0.2 an) (* 2.2 ao) (* 1.7 ap) (* 1.7 aq) (* 1.7 ar) (* 1.5 _as) (* 2.2 at) (* 1.9 au) (* 2.5 av) (* 2.8 aw) (* 1.5 ax) (* 0 ay) (* 6.1 az) (* 3.2 ba) (* 2.6 bb) (* 2.1 bc) (* 1.1 bd) (* 1.7 be) (* 2.8 bf) (* 0 bg) (* 1.5 bh) (* 1.6 bi) (* 1.7 bj) (* 1.8 bk) (* 2 bl) (* 0 bm) (* 3.9 bn) (* 4 bo) (* 1.8 bp) (* 1.6 bq) (* 2.3 br) (* 2.5 bs) (* 2 bt) (* 2.9 bu) (* 1.8 bv) (* 1.6 bw) (* 2.9 bx) (* 2.5 by) (* 3.9 bz) (* 1.6 ca) (* 2.7 cb) (* 3 cc) (* 1.8 cd) (* 1.5 ce) (* 1.8 cf) (* 2.3 cg) (* 1.7 ch) (* 1.7 ci) (* 2.9 cj) (* 0 ck) (* 0.5 cl) (* 0.4 cm) (* 0.8 cn) (* 12 co) (* 1.1 cp) (* 0 cq) (* 1.2 cr) (* 0.1 cs) (* 1.1 ct) (* 0.2 cu) (* 0.3 cv) (* 2.6 cw) (* 0.9 cx) (* 0.1 cy) (* 1.5 cz) (* 0.3 da) (* 1.3 db) (* 2.3 dc) (* 1 dd) (* 7.7 de) (* 14.6 df) (* 0.3 dg) (* 6 dh) (* 4.8 di) (* 2.6 dj) (* 0.7 dk) (* 1.7 dl) (* 0.1 dm) (* 1 dn) (* 1.1 do) (* 0.7 dp) (* 0.1 dq) (* 0.1 dr) ) 21))
(assert (>= (+ (* 2.3 aa) (* 2.5 ab) (* 3.3 ac) (* 2.5 ad) (* 3.1 ae) (* 2.1 af) (* 2.1 ag) (* 1.6 ah) (* 6 ai) (* 2.1 aj) (* 2.7 ak) (* 2.9 al) (* 4.4 am) (* 0 an) (* 2.5 ao) (* 2 ap) (* 1.8 aq) (* 2.9 ar) (* 1.9 _as) (* 2.7 at) (* 2.2 au) (* 2.1 av) (* 2.9 aw) (* 1.4 ax) (* 0.1 ay) (* 4.2 az) (* 2.4 ba) (* 2.6 bb) (* 1.6 bc) (* 1.6 bd) (* 2.1 be) (* 1.8 bf) (* 0 bg) (* 2.3 bh) (* 2.5 bi) (* 3 bj) (* 2.6 bk) (* 3.4 bl) (* 0.6 bm) (* 3.3 bn) (* 5.3 bo) (* 3.3 bp) (* 2.4 bq) (* 2.5 br) (* 3.1 bs) (* 3.3 bt) (* 3.8 bu) (* 3.6 bv) (* 2.3 bw) (* 4 bx) (* 3.4 by) (* 4.5 bz) (* 1.8 ca) (* 3.3 cb) (* 2.1 cc) (* 2.5 cd) (* 2.9 ce) (* 3.6 cf) (* 3.4 cg) (* 3.2 ch) (* 3 ci) (* 0.2 cj) (* 0 ck) (* 0.6 cl) (* 0.5 cm) (* 0 cn) (* 2.1 co) (* 2 cp) (* 0.4 cq) (* 1.9 cr) (* 0.2 cs) (* 1.6 ct) (* 0.1 cu) (* 0.2 cv) (* 3.9 cw) (* 1.3 cx) (* 0.7 cy) (* 0.8 cz) (* 0.5 da) (* 0.8 db) (* 0.4 dc) (* 0.6 dd) (* 3.6 de) (* 6 df) (* 0.5 dg) (* 1.1 dh) (* 0.8 di) (* 0.5 dj) (* 0.4 dk) (* 0.7 dl) (* 0.1 dm) (* 0.3 dn) (* 0.3 do) (* 0.3 dp) (* 0.6 dq) (* 1 dr) ) 5))

;; hints
(assert (<= (+ (* 395 aa) (* 545 ab) (* 532 ac) (* 441 ad) (* 498 ae) (* 478 af) (* 387 ag) (* 311 ah) (* 1067 ai) (* 428 aj) (* 527 ak) (* 489 al) (* 776 am) (* 38 an) (* 389 ao) (* 475 ap) (* 395 aq) (* 457 ar) (* 307 _as) (* 431 at) (* 345 au) (* 364 av) (* 465 aw) (* 256 ax) (* 60 ay) (* 979 az) (* 659 ba) (* 525 bb) (* 323 bc) (* 292 bd) (* 374 be) (* 319 bf) (* 121 bg) (* 419 bh) (* 420 bi) (* 550 bj) (* 396 bk) (* 695 bl) (* 1 bm) (* 553 bn) (* 768 bo) (* 728 bp) (* 486 bq) (* 594 br) (* 693 bs) (* 655 bt) (* 542 bu) (* 655 bv) (* 406 bw) (* 584 bx) (* 498 by) (* 709 bz) (* 356 ca) (* 724 cb) (* 434 cc) (* 473 cd) (* 642 ce) (* 625 cf) (* 471 cg) (* 579 ch) (* 558 ci) (* 83 cj) (* 31 ck) (* 287 cl) (* 23 cm) (* 10 cn) (* 1034 co) (* 252 cp) (* 8 cq) (* 249 cr) (* 6 cs) (* 243 ct) (* 275 cu) (* 148 cv) (* 810 cw) (* 270 cx) (* 109 cy) (* 145 cz) (* 33 da) (* 161 db) (* 304 dc) (* 211 dd) (* 1057 de) (* 1844 df) (* 44 dg) (* 517 dh) (* 410 di) (* 225 dj) (* 235 dk) (* 337 dl) (* 59 dm) (* 257 dn) (* 295 do) (* 232 dp) (* 108 dq) (* 7 dr)) 3500))
(assert-soft (and (>= ay 7) (>= bm 18) (>= cn 282)))

;; objective don't move this up
(minimize (+ (* 395 aa) (* 545 ab) (* 532 ac) (* 441 ad) (* 498 ae) (* 478 af) (* 387 ag) (* 311 ah) (* 1067 ai) (* 428 aj) (* 527 ak) (* 489 al) (* 776 am) (* 38 an) (* 389 ao) (* 475 ap) (* 395 aq) (* 457 ar) (* 307 _as) (* 431 at) (* 345 au) (* 364 av) (* 465 aw) (* 256 ax) (* 60 ay) (* 979 az) (* 659 ba) (* 525 bb) (* 323 bc) (* 292 bd) (* 374 be) (* 319 bf) (* 121 bg) (* 419 bh) (* 420 bi) (* 550 bj) (* 396 bk) (* 695 bl) (* 1 bm) (* 553 bn) (* 768 bo) (* 728 bp) (* 486 bq) (* 594 br) (* 693 bs) (* 655 bt) (* 542 bu) (* 655 bv) (* 406 bw) (* 584 bx) (* 498 by) (* 709 bz) (* 356 ca) (* 724 cb) (* 434 cc) (* 473 cd) (* 642 ce) (* 625 cf) (* 471 cg) (* 579 ch) (* 558 ci) (* 83 cj) (* 31 ck) (* 287 cl) (* 23 cm) (* 10 cn) (* 1034 co) (* 252 cp) (* 8 cq) (* 249 cr) (* 6 cs) (* 243 ct) (* 275 cu) (* 148 cv) (* 810 cw) (* 270 cx) (* 109 cy) (* 145 cz) (* 33 da) (* 161 db) (* 304 dc) (* 211 dd) (* 1057 de) (* 1844 df) (* 44 dg) (* 517 dh) (* 410 di) (* 225 dj) (* 235 dk) (* 337 dl) (* 59 dm) (* 257 dn) (* 295 do) (* 232 dp) (* 108 dq) (* 7 dr)))

;; solve the problem using the default solver
(check-sat)

;; print the value of the side salad variable at the optimum
(get-model)

実行すると次の結果が得られました。

% time ./z3 -smt2 mcdonalds.smt2
sat
(
  (define-fun bj () Int
    0)
  (define-fun db () Int
    0)
  (define-fun ak () Int
    0)
  (define-fun br () Int
    0)
  (define-fun co () Int
    0)
  (define-fun bk () Int
    0)
  (define-fun bl () Int
    0)
  (define-fun bo () Int
    0)
  (define-fun _as () Int
    0)
  (define-fun dr () Int
    0)
  (define-fun ay () Int
    7)
  (define-fun cc () Int
    0)
  (define-fun aj () Int
    0)
  (define-fun bp () Int
    0)
  (define-fun ct () Int
    0)
  (define-fun dm () Int
    0)
  (define-fun bz () Int
    0)
  (define-fun ah () Int
    0)
  (define-fun bt () Int
    0)
  (define-fun cm () Int
    1)
  (define-fun dc () Int
    0)
  (define-fun cz () Int
    0)
  (define-fun bn () Int
    0)
  (define-fun cd () Int
    0)
  (define-fun ci () Int
    0)
  (define-fun ab () Int
    0)
  (define-fun cf () Int
    0)
  (define-fun bh () Int
    0)
  (define-fun di () Int
    0)
  (define-fun bq () Int
    0)
  (define-fun dl () Int
    0)
  (define-fun an () Int
    2)
  (define-fun dq () Int
    0)
  (define-fun ai () Int
    0)
  (define-fun df () Int
    0)
  (define-fun cy () Int
    0)
  (define-fun aq () Int
    0)
  (define-fun bd () Int
    0)
  (define-fun am () Int
    0)
  (define-fun bw () Int
    0)
  (define-fun cr () Int
    0)
  (define-fun av () Int
    0)
  (define-fun ao () Int
    0)
  (define-fun cu () Int
    0)
  (define-fun bi () Int
    0)
  (define-fun dd () Int
    0)
  (define-fun cb () Int
    0)
  (define-fun cl () Int
    0)
  (define-fun cg () Int
    0)
  (define-fun bx () Int
    0)
  (define-fun ae () Int
    0)
  (define-fun ad () Int
    0)
  (define-fun dh () Int
    0)
  (define-fun ca () Int
    0)
  (define-fun cw () Int
    0)
  (define-fun ck () Int
    0)
  (define-fun aw () Int
    0)
  (define-fun au () Int
    0)
  (define-fun bv () Int
    0)
  (define-fun ax () Int
    0)
  (define-fun ba () Int
    0)
  (define-fun do () Int
    0)
  (define-fun ap () Int
    0)
  (define-fun bc () Int
    0)
  (define-fun by () Int
    0)
  (define-fun cj () Int
    0)
  (define-fun ar () Int
    0)
  (define-fun dp () Int
    0)
  (define-fun ag () Int
    0)
  (define-fun be () Int
    0)
  (define-fun cx () Int
    0)
  (define-fun at () Int
    0)
  (define-fun bm () Int
    18)
  (define-fun de () Int
    0)
  (define-fun dn () Int
    0)
  (define-fun bu () Int
    0)
  (define-fun cv () Int
    0)
  (define-fun dj () Int
    0)
  (define-fun ce () Int
    0)
  (define-fun bs () Int
    0)
  (define-fun dg () Int
    0)
  (define-fun af () Int
    0)
  (define-fun cn () Int
    282)
  (define-fun al () Int
    0)
  (define-fun aa () Int
    0)
  (define-fun cq () Int
    0)
  (define-fun az () Int
    0)
  (define-fun bb () Int
    0)
  (define-fun bf () Int
    0)
  (define-fun bg () Int
    0)
  (define-fun ch () Int
    0)
  (define-fun da () Int
    0)
  (define-fun dk () Int
    0)
  (define-fun ac () Int
    0)
  (define-fun cs () Int
    0)
  (define-fun cp () Int
    0)
)
./z3 -smt2 mcdonalds.smt2  0.10s user 0.02s system 61% cpu 0.197 total. occupied 68224 kilobytes at maximum.

ここまでヒントを与えれば、当初の想定通り、一瞬で終わりました。

結果が 0 でなかったものを確認します。

記号 品名 個数
ay バターパット 7
cm ケチャップ 1
an ストロベリージャム 2
bm 塩・コショウ 18
cn サイドサラダ 282

オチも同じになることを確認できました。

1時間で計算が終わらなかったことに比べれば、同じ結果になることに驚きはありませんね 😅

感想

最強の SMT ソルバー、Z3 で解いてみました。元記事と同じ条件では解けませんでしたが、カンニングに近いことをすれば解けました。そして、同じ結果になりました。

「ソルバー」と呼ばれるものにも色々な種類があり、それぞれ得意とする領域があります。マクドナルド問題はおそらく Z3 の能力を発揮しにくい課題で、かつデフォルトの optimizer が苦手とする問題だったため、私が与えたヒントによって力技で解くような形になってしまいました。

元記事がバズったということは、みんな数理最適化をやったことがないだけで、挑戦してみたいのだと思います。この分野にはピッタリはまらないかもしれませんが、Z3 の記事も増えたらいいなと思います。

関連記事

湯婆婆みたいにみんなで楽しむ流れかと思ったのに、参加者が少なくて残念です。みんなダイエット問題タグで書けばいいのにと思います。

他にも1つだけ、元記事とできるだけ条件を揃えて解を求めようとした記事があり、驚いたことに量子コンピューターを使われていましたので、こちらで紹介させていただきます。それぞれの解法に向き不向きがありそうで、面白いですね。今回は Z3 の強さをお見せできなかったのが残念です。

また、バズった元記事よりも先に同じことに挑戦されていた方の記事や、続編記事もありましたので、合わせて紹介させていただきます。

  1. 以前は最強と言われていたはずですが、情報が古かったようで、今 SMT-COMP 2020 Results を見たら CVC4 が席巻していました。@masahiro_sakai さんも唯一の CVC4 タグ記事、DEF CON CTF 2016 Qualifiers のbaby-re問題のメモで使われています。 ↩

  2. νZ - Maximal Satisfaction with Z3 ↩ ↩2

  3. ほんとは assert を使っても結果が出なかった時点で自力解決は諦めていたのですが、散歩中にひらめきました ↩

  4. 元はといえば、こうした使い方をされるようになったことが、このオマケ機能が追加された理由のようです2。 ↩

8
5
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
8
5

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?