主張が常に成り立つか調べる
SMTソルバーとは、条件に合う値を探し、なければ「ない」と答えるプログラムです。Z3 はその代表で、「この主張は、どんな値でも成り立つか」を機械に尋ねられます。
100円ごとに1ポイントがたまる店で、「ポイントは金額を超えない」と言いたいとします。金額が負なら、この主張は崩れます。ソルバーは、その負の金額を見つけてくれます。
このレッスンのゴール
メモ
主張がいつも成り立つかを、Z3 に尋ねて読み取れる。
重要な言葉
| ことば | いみ | れい |
|---|---|---|
| ソルバー | 条件に合う値を探す道具 | Z3 |
| 充足可能 | 条件に合う値が1つ以上ある（sat） | |
| 充足不能 | 条件に合う値が1つもない（unsat） | |
| モデル | 条件に合う値の1組 | n = 4 |
| 主張 | いつも成り立つと言いたい文 | |
| 反証 | 主張の反対を成り立たせる値を探すこと |
学生が入力するセルは、このプレビューでは空白です。
Z3は条件に合う値を探す
Z3 に尋ねるには、3つのことをします。探したい数に名前をつけ（declare-const）、条件を並べ（assert）、check-sat で尋ねます。
式は、演算子を先に書きます。(> n 3) は n > 3 の意味で、(+ a b) は a + b の意味です。答えは、条件に合う値があれば sat、なければ unsat です。
nは3より大きく6より小さい
echo '(declare-const n Int) (assert (> n 3)) (assert (< n 6)) (check-sat) (get-value (n))' | z3 -inここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
合計1000円で兄は3倍出す
echo '(declare-const a Int) (declare-const b Int) (assert (= (+ a b) 1000)) (assert (> a 0)) (assert (> b 0)) (assert (= a (* 3 b))) (check-sat) (get-model)' | z3 -inここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
合計が1001円なら
echo '(declare-const a Int) (declare-const b Int) (assert (= (+ a b) 1001)) (assert (= a (* 3 b))) (check-sat)' | z3 -inここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
主張は反対を探して証明する
主張がいつも成り立つかを知りたいときは、「主張が成り立たない値があるか」を尋ねます。これが反証です。
unsat なら、反対になる値は1つもありません。つまり、主張はいつも成り立ちます。sat なら、出てきた値が反例です。
Z3の答えの読み方
| 尋ねたこと | 答え | 意味 |
|---|---|---|
| 主張そのもの | sat | 成り立つ場合がある（証明ではない） |
| 主張の反対 | unsat | 主張はいつも成り立つ（証明） |
| 主張の反対 | sat | 反例が見つかった |
学生が入力するセルは、このプレビューでは空白です。
前提を置くと証明できる
100円ごとに1ポイントなら、ポイントは n div 100 です。div は、割って小数点以下を捨てる割り算です。主張は「ポイントは金額 n 以下」です。
まず「n は0以上」という前提を置いて、反対を尋ねます。次に、前提を外して尋ねます。
0円以上ならポイントは金額以下
echo '(declare-const n Int) (assert (>= n 0)) (assert (not (<= (div n 100) n))) (check-sat)' | z3 -inここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
前提を外して反例を探す
echo '(declare-const n Int) (assert (not (<= (div n 100) n))) (check-sat) (get-model)' | z3 -inここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
よくある間違い
注意
主張の反対を尋ねて sat と出たら、証明できた、と思いがちです。逆です。反対の sat は、反例が見つかった、という意味です。証明できたのは、反対を尋ねて unsat と出たときです。
PythonからもZ3を使える
ラボには、Python 用の Z3 も入っています。同じ尋ね方を、Python の文で書けます。
次のコマンドは、7で割ると3余り、5で割ると2余る正の整数 n を探します。s.add が条件を足し、s.check() が sat か unsat を返します。
Pythonから尋ねる
python3 -c 'from z3 import *; n = Int("n"); s = Solver(); s.add(n > 0, n % 7 == 3, n % 5 == 2); print(s.check()); print(s.model())'ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
さらに挑戦: 負の数と割り算
課題が通ったら、n // 100 <= n の範囲を -300 から300にして、最初の反例を Python で探しましょう。
次に、Z3 の (div n 100) と、Python の n // 100 が、負の数でも同じ答えを出すか、-1 と -99 で確かめます。2つの言語で、割り算の決まりが違うことがあります。