この記事を書くにあたり

今私は契約社員ではあるが、
ベンチャー企業にて開発部門にて戦力になるべく奮闘中。
少し客観的な視点でここまでの道のりと今後の目標などを踏まえ、
反省点なども含め時系列で整理していこうと思う。
また、未経験スキルでの転職のリアル感が伝わればどんな感じで転職の道が進んでいくのか、
よりわかりやすいと思うのでその辺も書いていきたいと思う。

簡単な経歴

• 高校を卒業してインフラ系の会社に入社。

  • 数年間、機械や装置を扱うオペレーターを担当、簡単なシーケンスなども作成。

• 1社目のインフラ系の会社を辞める半年前にプログラミングスクールに入校。

  • 選択した言語はJavaとSwift。

• 空白期間を経て、コールセンターへ入社。

  • 担当はテクニカルサポート。

• SES会社へ入社。

  • 緊急事態宣言の影響でどこへもアサインできず社内待機を過ごす。

• コールセンターへ入社。

  • 経験を生かしてテクニカルサポートを担当。

• テスター求人を見てベンチャー企業へ入社。

  • 現在に至る。

全くの未経験期間

プログラミングスクールを探すまで

今でこそ、転職のノウハウは良い意味でも悪い意味でも慣れた物だが、まず、10年もいた会社から転職するということが未知の世界であったため、何をして良いか分からない状態であった。
電車の中吊りで転職サイトの広告を見て気になるなと思う程度でその先はどうなっているのかすらわからないって感じ。
なので、転職について色々とググってみたりYouTubeを見たりしたものだった。

この状態では正しい情報を見つけ出すのって相当難しい。
少し端折るが、そんなこともありパソコンのスキルが相当落ちていたと実感し、先ずはスクールを探した。
結局は実際に校舎がある老舗のスクールへ入校した。
結果的には、当時の自分にとっては問題ない入校だった。
なぜなら、当時は分からなかったがパソコンのスペックもエンジニアが持つ物ではなかったので結果的によかったと思う。
その程度の知識であったのだった。

入校後の受講プログラム

当時受講したのが、JavaとSwift。
正確に言えばAndroidとiPhoneアプリ作成コース。
なぜこのコースを選んだかといえば、単純にアプリを作ってみたかったからということと、
メジャーな言語であるJavaも習うことができるということ。
結果的にこのコースを選んだのは少し遠回りだった気もした。
Web制作コースやPHP、JSなどの言語を選んでおけばとも後々思ったりもしたが、
今の仕事をしている段階では全く役に立たないとも思ってはいない。
幅広い視点を持つことは全然問題ないことでもあるし、
情報系などの大学も出ていない私にとってJavaは言語の基礎を教えてくれたと言っても過言ではないだろう。
その後で、自分で調べて学べば良いという思考になったので、あとは何も問題ない。
話を戻すと、Javaを中心に受講させてもらい、オマケ程度にアプリ作成といった感じで半年ほどで受講を修了した。
コンパイルとは何か。
２進数、16進数、、、
機械語とは。
などなど
少しアカデミックなことを触れてコーディングに入っていき、
演習問題の繰り返しだった。

初めての転職フェア

そんなこんなで1社目はさっさと辞めてしまわないと辞めづらく、精神的にももたないので、
転職ができなくても辞めるつもりでいた。
とはいえのんびり転職を待つのもよくないので、
先ずは転職フェアに参加してみることにした。
知っている人なら知っている転職フェア。
あれはいわゆるSESフェア。
まあ、わかるとは思うが行かない方が良い。
分からない人にとってはIT業界ってああいうところなんだと洗脳されかける。

面接を受けてみたり、エントリーをしてみるがが上手くいかない。

コールセンター（テクサポ）へ

そんなこんなで仕事をしないのもよくないので、
コールセンターへ流れ着く。
転職後はほとんどをコールセンターで過ごすことになる。

朝活でPHP

コールセンターにずっといるわけにもいかないので、
朝の喫茶店で毎日就業前にPHPの勉強をすることにした。

緊急事態宣言を抜けてのベンチャーへ

色々あってコールセンターを行き来するのだが、
ようやくベンチャーでテスター業務から携わることになるわけだった。
それができたのも、
結局はReactでFirebaseにデプロイまで行けた知識を持てたということ。
コードを書いているだけでは話が薄っぺらくなってしまう。
そして、入社して思うのは実務経験に勝るものはないということ。
お金を貰いながらその業務に専念することでのスキルアップは格段に違う。
ようやく、ポジションに来れたのだから、
コーディングだけでなく、テストケースの作成、サーバー、インフラ側の知識、RDBやAPIのことなど、
いままで自分だけでは時間を割くことができなかったことにもやっていくことができるのではないだろうか。
周囲の優秀なエンジニアに囲まれて仕事ができることがいかに幸せなことか、
昨今の転職の大変さを聞いてよく身に染みる。

今も少しずつコーディングをしているが、
EC2ぐらいを使って繋げられたらと思っている。

JenkinsやCircleciを使って自動テストの知識についても増やしていきたい。
AWSを学ぶのならDockerもやりたいわけだ。

学ぶことは多い。
フロントの勉強をしていると、
限界を感じることが多く、
向上心があればどうしてもインフラ周りにいきたくなる。
なるほど、フロント側にフルスタックが多いのも納得と思った今日この頃。

※本稿はAtCoderProblemsのBeginnerContest,A~C問題をJavaを用いて地道に解いていく人間の観察日記です

目次

• まえがき
• AtCoder Beginner Contest 193に挑戦
  • A問題
  • B問題
  • C問題
• 感想
• お世話になったサイト（参考に使用）

まえがき

　アルゴリズムの勉強を行っているものの、自分が研究している狭い範囲から一歩外に出たら空で答えることができない..。まあそれでもいいか、と思ってはいたものの、プログラミングを勉強してからブランクが2年ほど空いている状況に危機感を覚えた為、せめて基礎基本をやり直したいと思い、始めてみました。

　つたないプログラミングが目立つかもしれませんが、何かの参考になったり、初心者向けにこんなトレーニングもあるよ！というものを共有していただけたりしたらな..と思います。

AtCoder Begginer Contest 193に挑戦

A問題

193A.java

import java.util.*;

class Main{

  public static void main(String args[]){

    Scanner sc = new Scanner(System.in);

    //入力された整数
    double A = sc.nextInt();
    double B = sc.nextInt();

    //計算するよ
    //[定価]-x*[定価]=売値
    //xが求めるパーセント
    double x = ( (A - B) / A ) * 100;

    //出力
    System.out.println(x);
  }
}

　実はScannerを完ッ全に忘れていた自分。まあ調べて使いこなしたししししし..大丈夫かな？

B問題

193B.java

import java.util.*;

class Main{
  public static void main(String args[]){
    Scanner sc = new Scanner(System.in);

    //最小の金額の為の数字
    int money = -1;

    //件数と言う名の行列の行の数
    int N = sc.nextInt();

    //ここから情報収集タイムゥ～～！！
    for(int n = 0; n < N; n++){
      int A = sc.nextInt();
      int P = sc.nextInt();
      int X = sc.nextInt();

      //0.5,1.5,2.5,...のやつを考慮
      //A分後にはすでにA台売切れてるってことじゃん
      //売切れてるか確認！
      if(X > A){//売切れてない&&最小なら
        if(money == -1 || money > P){
          money = P;
        }
      }
    }

    //出力
    System.out.println(money);
  }
}

　.......Scanner神
　そう感じた瞬間でした。直感でわかりやすい！なんで忘れていたんだ。実は昔、配列を作って、スペースor改行したら～みたいなことをしてました。とりあえず超面倒くさいことをしてたのです。よかつたよかつた。

C問題

193C.java

import java.util.*;

class Main{
  public static void main(String args[]){
    Scanner sc = new Scanner(System.in);

    //入力されたN(intだと足りない？)
    long N = sc.nextLong();

    //HashSetを使ってみようのコ～ナ～
    //取得順は適当だが、要素の重複不可、null格納可
    HashSet hs = new HashSet();

    for(long n=2; n*n<=N; n++){
      //下準備
      long calc = n * n;
      //計算結果の格納
      while(calc <= N){
        hs.add(calc);
        calc = calc * n;
      }
    }

    //N-[hashのsize] が求める値
    long ans = N - hs.size();
    System.out.println(ans);
  }
}

　intで変なエラーでるなと思ってたらlongってあったな..。完全にintとdoubleしか覚えていなかった。
　加えてHashSetも忘れてました。そういえばあったなと..。重複なしが便利な時代。高速で凄く助かりました。実は最初はfor文2回してcount変数作ってやってました。

☆エラーコード例

193C_Miss.java

import java.util.*;

class Main{
  public static void main(String args[]){
    Scanner sc = new Scanner(System.in);

    //入力されたN
    int N = sc.nextInt();

    //HashSetを使ってみようのコ～ナ～
    //取得順は適当だが、要素の重複不可、null格納可
    HashSet hs = new HashSet();

    for(int a=2; a<=N; a++){
      for(int b=2; b<=N; b++){
        //Math.powメソッドによる累乗計算
        int result = (int) Math.pow(a, b);
        //ここで数字がデカいならbreakする
        if(result > N) break;
        //ハッシュに追加
        if(result <= N) hs.add(result);
      }
    }

    //N-[hashのsize] が求める値
    System.out.println(N - hs.size());
  }
}

　これは間違った（実行時間が超長い）ものなのですが、最初は全然わかりませんでした(;・∀・)

　Math.powを使って華麗に解いてやるぜ！と思ったものの、累乗は負担が大きいみたいですね..。少し文を変えるだけで負担が減る。学びを得ましたよ。ホントにアルゴリズム勉強してる？と聞かれたら汗を大量に流すところでした。あぶないあぶない（アウト）。

　あとはwhile文を使うことに慣れたほうが良かったと思いました。for文ばかり使うって初心者あるあるじゃないですか(笑)

感想

　こ れ か ら も 続 け ま す ！そう思える3時間でした。ちなみに、先ほどの実行時間が長いものはO(n)。正解のものはO(log n)だそう。まあそうなんだけど..今言われたらなんとなく覚えてたけど..。

　とりあえず続けれるところまでは地味～～にやっていきます。時間の使い方が下手なことが致命傷な自分ですが、気楽に観ていただけると幸いです。Java初心者の方は一緒に頑張りまショ..。

　いや、プログラミング頑張った自分偉い！生きていて偉い！Fooo!!

お世話になったサイト

ほとんどここが検索TOPで出てきました。ありがたや..
https://techacademy.jp/magazine/category/programming/java

背景

会社の査定目標でJavaとAWSで何か作成します！と記入したものの先延ばしにしている内に結局
何も作れず査定日に近づいてしまったので、もうHello Worldレベルでもいいので何か
しなくてはということで取り組みました(実は提出義務はないので正直に作る必要も
本当はないのですが)。
作るの簡単だけど何か頑張ってそうに見えるAWS×Javaの成果物アイデアが別に何かあればぜひ
お教えください。非常に喜びます！

概要

AWSコンソールのLambda上から、maven projectをpackage化したJarファイルを起動します。

①Mavenプロジェクトの作成

Eclipse上で適当にMaven Projectを作成します。

②Lambdaの実行対象であるJavaクラスを作成

これもシンプルに作成します。argはLambdaから渡される引数です。

package qiitaLambda;

public class Qiita {
    public static String handleRequest(String arg) {
     return arg + "20210301";
    }
}

③Jarファイルを作成する

プロジェクト名を右クリック→実行(R)→Mavenビルドで設定画面を開き、設定画面上でゴール(G)にpackageと入力し実行します。

④AWS Lambdaコンソール上で関数を作成する。

⑤Jarファイルをアップロードする

⑥ランタイム設定を行う

ハンドラを{package名}.{クラス名}::{メソッド名}に変更します。

⑦テスト設定をする

画面右上のテストを押下すると設定画面が出るのでイベント名とその内容を書きます。ここではシンプルに文字列のHelloを記載し、これが②の関数のargに渡されます。

⑧テストをする

もう一度画面右上のテストを押下するとLambda関数が実行されます。実行結果を見ると⑦のようにLambdaで記述したHelloとあらかじめ②のJavaクラスで記述していた日付を結合して表示しているのでJarファイルを呼べていることが確認できます。

感想

背景でも述べさせていただきましたが、作るのは簡単だけど何か頑張ってそうに見えるAWS×Javaの成果物アイデアが別に何かあればぜひぜひお教え下さい！

実務で絶対使うと言っても過言ではないではないので、簡単にまとめました。

パッケージ

簡単に言うとグループ(パッケージ)を作ってクラスを分かりやすくすること

（例）車を作るとします

車を作るのに様々なクラス(部品)が必要で、組み合わせることで車が出来上がります。
図のようにグループわけをすることによってクラスが見やすくなり、変更・追加が楽になります。
クラスが増えれば増えるほど、パッケージの必要性が感じると思います。
ソースはインポートで見ていきましょう。

インポート

簡単に言うと他のクラスを呼び出し使うことができます。

（例）車を作るとします

ソースの階層はこんな感じです。
Main.javaで他のクラスを呼び出し、車を作りたいと思います。

まずはクラスから

Exterior.java

package exterior;

public class Exterior {
    public void bon() {
        System.out.println("ボンネット");
    }

    public void mirror() {
        System.out.println("ミラー");
    }

    public void taiya(){
        System.out.println("タイヤ");
    }

    public void glass() {
        System.out.println("ガラス");
    }
}

Interior.java

package interior;

public class Interior {

    public void air(){
        System.out.println("エアコン");


    public void handle(){
        System.out.println("ハンドル");
    }

    public void seat(){
        System.out.println("座席");
    }
}

Other.java

package other;

public class Other {

    public void engine(){
        System.out.println("エンジン");
    }

    public void scarf(){
        System.out.println("マフラー");
    }
}

ここまででパッケージでも説明したようにクラス分けができていると思います。
では、クラスを呼び出していきましょう。

Main.java

package main;

import exterior.Exterior;//外装呼び出し
import interior.Interior;//内装呼び出し
import other.Other;//その他呼び出し

public class Main {

    public static void main(String[] args) {
        //インスタンス
        Exterior e = new Exterior();
        Interior i = new Interior();
        Other o = new Other();

        //外装
        e.bon();
        e.mirror();
        e.taiya();
        e.glass();

        //内装
        i.air();
        i.handle();
        i.seat();

        //その他
        o.engine();
        o.scarf();
    }

}

//実行すると
ボンネット
ミラー
タイヤ
ガラス
エアコン
ハンドル
座席
エンジン
マフラー

このようにインポートを使って他のクラスを呼び、車が出来上がります。
あくまで、ここでは例ですけど、流れはこんな感じです。

#Javaで学ぶアルゴリズム < 数値積分 >

はじめに

Javaは授業で触れただけで全くの初心者であり，何もわかっていない．なので，基本的なアルゴリズムをJavaで実装し，アルゴリズムの理解を深めるとともに，Javaにも慣れていきたい．
その第8弾として数値積分を扱う．

数値積分

数学的計算であれば，数値積分を使うことも少ないのかもしれない．しかしながら，システム的制御など，動的な系の中で，積分を行うとなれば，数値積分が非常に重要となってくる．その数値積分にもいくつかの方法が存在する．ここでは，台形則・シンプソン則の2つほど例に詳しく見ていき，その他は名前とちょっとした特徴に触れる程度とする．

原理

比較

違いとしては，台形則が直線での近似であるのに対して，シンプソン則は2次曲線での近似である．これにより，計算上は，シンプソン則の方が，誤差を小さくできるという．詳しくは後に記述する．

実装

先ほどの説明に従い，Javaでの実装を行う．ここでは，被積分関数を$\sqrt{4-x^2}$として，積分により$\pi$を求めるものとする．以下にソースコードとそのときの出力を示す．

ソースコード

integral1.java

//2021/02/27
//@Yuya Shimizu
//---------------------------
//*     数値積分（台形則） *
//---------------------------

import java.awt.*;
import java.awt.event.*;


//フレームの設定
class integral1_Frame extends Frame{
    private TextArea ta;
    private TextField tf1, tf2;
    double f(double x){     //被積分関数
        return Math.sqrt(4 - x*x);
    }
    public integral1_Frame(){
        setSize(300, 200);//300×200の大きさでフレームを作成
        //×ボタンを押したら終了
        addWindowListener(new WindowAdapter(){
            public void windowClosing(WindowEvent e){
                System.exit(0);
            }
        });
        Panel p;    //パネル変数
        Button bt;  //ボタン変数

        add(p = new Panel(), "North");  //フレーム上側にパネルを貼り付け
        p.add(new Label("積分区間"));   //先ほどのパネルにラベルを貼り付け
        p.add(tf1 = new TextField("", 6));  //先ほどのパネルにテキストフィールドを貼り付け
        p.add(tf2 = new TextField("", 6));  //先ほどのパネルにテキストフィールドを貼り付け

        add(ta = new TextArea(5, 40), "Center");    //フレーム中央にテキストエリアを貼り付け
        add(bt = new Button("計算"), "South");    //フレーム中央にテキストエリアを貼り付け

        //ボタンの設定
        bt.addActionListener(new ActionListener(){
            public void actionPerformed(ActionEvent e){
                int k;
                double a, b, n, h, x, s, sum;
                a = Double.parseDouble(tf1.getText());
                b = Double.parseDouble(tf2.getText());
                n = 50;     //a~bの分割数
                h = (b-a)/n;    //区間幅
                x = a;
                s = 0;

                for (k=1; k<=n-1; k++){
                    x = x + h;
                    s = s + f(x);
                }
                sum = h * ((f(a) + f(b))/2 + s);
                String result = "     /" + b + "\n" + 
                                "     | sqrt(4-x*x) =" + sum + "\n"+
                                "     /" + a;
                ta.setText(result);
            }
        });
    }
}

//クラス
public class integral1{
    //メイン関数
    public static void main(String[] args){
        Frame w=new integral1_Frame();
        w.show();
    }
}

出力

実行前

実行後

ソースコード（シンプソン則）

integral2.java

//2021/02/27
//@Yuya Shimizu
//-----------------------------------
//*     数値積分（シンプソン則）    *
//-----------------------------------

import java.awt.*;
import java.awt.event.*;


//フレームの設定
class integral2_Frame extends Frame{
    private TextArea ta;
    private TextField tf1, tf2;
    double f(double x){     //被積分関数
        return Math.sqrt(4 - x*x);
    }
    public integral2_Frame(){
        setSize(300, 200);//300×200の大きさでフレームを作成
        //×ボタンを押したら終了
        addWindowListener(new WindowAdapter(){
            public void windowClosing(WindowEvent e){
                System.exit(0);
            }
        });
        Panel p;    //パネル変数
        Button bt;  //ボタン変数

        add(p = new Panel(), "North");  //フレーム上側にパネルを貼り付け
        p.add(new Label("積分区間"));   //先ほどのパネルにラベルを貼り付け
        p.add(tf1 = new TextField("", 6));  //先ほどのパネルにテキストフィールドを貼り付け
        p.add(tf2 = new TextField("", 6));  //先ほどのパネルにテキストフィールドを貼り付け

        add(ta = new TextArea(5, 40), "Center");    //フレーム中央にテキストエリアを貼り付け
        add(bt = new Button("計算"), "South");    //フレーム中央にテキストエリアを貼り付け

        //ボタンの設定
        bt.addActionListener(new ActionListener(){
            public void actionPerformed(ActionEvent e){
                int k;
                double a, b, n, h, fo, fe, sum;
                a = Double.parseDouble(tf1.getText());
                b = Double.parseDouble(tf2.getText());
                n = 50;     //a~bの分割数
                h = (b-a)/(2*n);    //区間幅
                fo = 0;
                fe = 0;

                for (k=1; k<=2*n-3; k=k+2){
                    fo = fo + f(a+h*k);
                    fe = fe + f(a+h*(k+1));
                }
                sum = (f(a)+f(b)+4*(fo+f(b-h))+2*fe)*h/3;
                String result = "     /" + b + "\n" + 
                                "     | sqrt(4-x*x) =" + sum + "\n"+
                                "     /" + a;
                ta.setText(result);
            }
        });
    }
}

//クラス
public class integral2{
    //メイン関数
    public static void main(String[] args){
        Frame w=new integral2_Frame();
        w.show();
    }
}

出力

実行前

実行後

注意

はじめに少し触れたが，ここで数値積分の誤差についてもう少し詳しく見ていくこととする．単純には，誤差は（台形則）>（中点則$^{(1)}$）>（シンプソン則）のようになる．ただし，周期関数の1周期にわたる積分では，台形則・中点則はきわめて高い精度が得られる．さらに，理論上は，台形則・中点則の誤差オーダーは分割数の2乗に反比例するので，分割数を10倍にすれば，1/100オーダーで精度が高くなる．しかし，コンピュータの有効桁数を超す精度は得られないので，分割数を過度に大きくしすぎると，逆に丸め誤差$^{(2)}$に蓄積され，逆に精度が落ちることに注意．

---

(1) 中点則：台形則とほとんど同じだが，台形則でh幅で計算していた各面積をさらに半分のh/2幅で計算する方法．
(2) 丸め誤差：有効桁数になるよう四捨五入するときに，計算機内部で発生する誤差．

その他の数値積分

先ほどの台形則・中点則・シンプソン則はまとめて，ニュートン・コーツ(Newton-Cotes)系の公式として知られ，区間を等間隔に分割する方法である．その他2つをここでは示すこととする．

チェビシェフ(Chebyshev)の公式

区間を不等間隔で重みを一定にする方法

ガウス(Gauss)の公式

区間を不等間隔で重みも一定でない方法．
もっとも精度が高い

感想

今までに，大学の授業でも数値積分を扱ったことはあった．そのときは台形則を用いていた．今回は，それを改めて復習できたことに加えて，ほかの数値積分の方法を学ぶことができた．ロボットの制御，特に移動を伴うような場合には，数値積分にお世話になることも多くなるかもしれないので，そのときにいくつかの選択があるということを意識しておこうと思う．（それぞれの方法に特徴があるため．）
数値計算についての学習はもうしばらく続く．数学的な部分が多いが，これらも制御系では役立つと思って，士気を高めて頑張っていきたい．

参考文献

Javaによるはじめてのアルゴリズム入門　　河西 朝雄　著　技術評論社

これは友達向けのJavaの小テストです。
Java初心者の文法腕試しでお使いくださいー！！

今日はwhile文の小テストを作りたいと思います！

問題①：次のプログラムを10未満の偶数の数を出力するように訂正せよ。

while(i < 10) {
    System.out.println(i);
}

問題②：次の出力は何か？

public class WhileClass {
    public static void main(String[] args) {
       int i = 0;
       while(i < 10) {
           if(i % 3 == 0 && i % 5 == 0) {
               System.out.println("FizzBuzz");
           } else if(i % 3 == 0) {
               System.out.println("Fizz");
           } else if(i % 5 == 0) {
               System.out.println("Buzz");
           } else {
               System.out.println(i);
           }
           i++;
       }
    }
}

問題③：次の問題に答えよ

for文とwhile文はどのように使い分けるか？

問題④：以下を全て満たすプログラムをwhileを使って書け。

• ユーザーに2つの数字の入力を求める。
• 入力が数字でない場合は, 聞き直す。
• 入力後
  • 入力が0であれば, プログラムは終了
  • 入力が1であれば, 2つの数を足した値を返す
  • 入力が2であれば, 2つの数を引いたの絶対値を返す。
  • 入力が3であれば, 2つの数をかけた数を返す。
  • 入力が4であれば, 大きい方から小さい方を割った数を返す。(ただし, 小さい数が0だった場合はエラーを出力）
  • (入力が5であれば, 数字を聞き直す。) ← 出来れば。

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

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 タグの記事があることからその人気をご理解いただけると思います。最適化問題を解くこともでき²、オマケ機能とはいえ、ダイエット問題ならば解けそうな気がします。

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

チュートリアルを試す

しかし、私は最適化のために 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 と違ってエラーは出さずに頑張ってくれています。

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

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

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

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

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

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 ↩

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

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