ライブラリZ3入門（ソルバー）

１．はじめに

これからのプログラミングは、コンピュータに「 手順 」を教えるのではなく、「 ゴール 」を示す方式になるでしょう。（注：あくまで筆者の見解・予測です）

もう少し詳しく言うと、これまでのプログラミング（ここでは、「古典的プログラミング」と言うことにします）では、プログラマが問題解決の 手順 を考え、その手順をコンピュータに教えて（コーディングして）問題を解かせていました。しかしこれからのプログラミング（ここでは、「新プログラミング」と言うことにします）では、「こういう条件を満足するためにはどうであれは良いか」をコンピュータに問う、つまり ゴール （目標、満足すべき条件・状態）を示してそのための解（答え）を出させるというようになるでしょう。　そのため、これからはこの新プログラミングに沿ったスキルを身に着け、この方式に合ったツールを使いこなせるようになる必要があるでしょう。

現在でもこのようなツールは存在しており、それらは「ソルバー」と呼ばれています（直訳すると「解決者」）。これらは、組み合わせ問題の分野でよく使われています。例えば、連立方程式の解を求めたり、魔方陣や数独の答を示してくれたり、巡回セールスマン問題を解いたりします。

２．ソルバーについて

Z3ライブラリ

Pythonで使えるソルバーのひとつとして、 Z3 というライブラリがあります。 Z3Py と表記されることもあります。

• 公式ページ https://github.com/Z3Prover/z3

• 参考ページ

  • SMTソルバー Z3Py （@Ganesha） https://qiita.com/Ganesha/items/7a606ffc8a7c2504c143
  • Z3入門の入門（@kaizen_nagoya(Dr. Kiyoshi Ogawa)） https://qiita.com/kaizen_nagoya/items/87199127233646d5db07

Z3ライブラリのインストール

Z3ライブラリは外部ライブラリなので、インストールする必要があります。（外部ライブラリのインストールについては、「外部ライブラリのインストール方法」を参照してください）

注意

「 z3 」をインストールしないでください！ソルバーは「 z3-solver 」です。

Thonyエディタなどで、PyPIで ”z3” で検索すると「 z3 」というライブラリが見つかることがありますが、これのコメントを確認してみてください。「Backup ZFS snapshots to S3」と書かれていたら、これはソルバーのz3では ありません 。ソルバーのz3は「z3-solver an efficient SMT solver library」などと書かれているので、この「 z3-solver 」の方をインストールしてください。紛らわしいですが、間違えないようにしてください。

コマンドラインでインストールする場合も、 pip install z3-solver となります。

（参考） 表計算ソフトのExcelにもソルバー機能はあります。また、連立方程式を解くソルバーとしては、 Sympyライブラリ や Numpyライブラリ のsolve( )を使う方法もあります。各自で調べてみてください。

３．この教材の目的

この教材の目的は、Z3などのプログラムを 書けるようになることではありません 。そうなればベストですが、ここではむしろ、プログラムを 読めるようになること を目指しています。実際、今後はプログラムを書くこと自体は 生成AI に任せるようになるでしょう。しかし、そのプログラムが自分の要望を正確に実現しているかは、自分で確認しなければなりません。また、そもそも生成AIにどのような指示（プロンプト）を与えれば要望通りの結果を出すのかといったことが今後重要になってくるでしょう。そのためにも、AIが出した結果を読める必要があります。

以下で【応用】などでコードを改造する話も出てきますが、自分でプログラムを書いても良いですし、生成AIに質問するのも良いでしょう。（両方やればかなりのスキルアップになります）

• 生成AIの例 ※最初に使う時はID新規作成・登録などが必要な場合があるかもしれません

  • Chat-GPT
  • Perplexity

  その他、論理的な問題に強いモデルなどもありますので、調べてみてください。

注意

生成AIが出力したコードをそのまま実行しても、エラーが出て動かないという場合が 多々 あります。その場合は、「このコードではｘｘｘというエラーが出て動きません。修正してください」のように、追加で指示すると良いでしょう。生成AIとの付き合い方もこの機会に学んでみてください。

４．Z3のコードを読む

（１）生成AIを用いたプログラミングをしてみる

まずは生成AIでプログラムを作ってみましょう。Chat-GPTやPerplexityで、

「 Z3pyを使って、2*x+1=5を満たすxを求めるプログラムを書いて下さい 」

と質問してみましょう。生成AIによって多少異なりますが、たいていは次のようなプログラムになると思われます。ここではこのプログラムで説明を進めます。

なお、生成AIはプログラムだけではなく解説も表示する場合もありますので、そちらも参考にして学んでいくと良いでしょう。

（２）コードの流れ

Z3は様々な使い方がありますが、以下によく使われている簡単な例で説明します。この流れを頭に入れておけば、Z3のコードは読みやすくなります。

下記のプログラムコードを自分のPythonエディタにコピーして実行してみてください。（z3-solverのライブラリは事前にインストールしておいてください）

from z3 import *        #<1>インポート

X = Int("x")            #<2>変数作成

s = Solver()            #<3>ソルバーの作成

s.add(2*X + 1 == 5)     #<4>条件追加　※この部分を色々変えて実行してみてください。

r = s.check()           #<5>ソルバー実行
if r == sat:            #<6>条件に合う解があるか判定　注）"sat"は変数ではなく、Z3のシステム定数
    print(s.model())    #<7>解があれば結果表示
else:
    print("解無し")      #<8>解がなければメッセージ表示

#結果表示
# [x = 2]

（３）変数作成について

上記の例では、プログラム中で使う変数は X、結果表示の時などにユーザーが識別できるようにするのを x として作成しています。ここで作成された X は一般の整数型変数ではなく、Z3のオブジェクトの整数型変数です。Int( ) の頭文字が大文字であることに注意してください。このため、これらのZ3のオブジェクトをPythonの一般の関数の中で使うと、意図しない結果になることがあります。Z3のオブジェクトはZ3の関数（And、Sum、Ifなど、頭文字が大文字）で使うようにするとよいでしょう。

• 変数名のリスト（1次元配列）

この例では、変数は x だけでしたが、Z３では多数の変数を使うことがしばしばあり、このような場合は 変数名のリスト（配列） を作ることがあります。この場合、 ％書式 とfor文の 内包表記 を使って効率的に作成することができます。これは後述の「10桁の整数を生成する例」で使っています。（なお、下記の例では書式に%dを使っていますが、資料によっては%sとしているものもあります。）

from z3 import *
X = [Int("x_%d" % i) for i in range(3)]
print(X)

# [x_0, x_1, x_2]

• 変数名のリスト（2次元配列）

また、この方法で２次元配列も作ることができます。これは後述の「魔方陣の例」で使っています。

from z3 import *
X = [[Int("x_%d_%d" % (i, j)) for j in range(3)] for i in range(3)]
print(X)

# [[x_0_0, x_0_1, x_0_2], [x_1_0, x_1_1, x_1_2], [x_2_0, x_2_1, x_2_2]]

なお、上記の％書式とfor文の内包表記を使わずに、 IntVector( ) 関数 などを使って作成することもできます。生成される変数名は自動的に、引数で指定した文字に”__” （アンダーバーが２つ）と数字を付けたものになります。

from z3 import *
X = IntVector("x",3)
print(X)

# [x__0, x__1, x__2]

（４）条件追加について

• 様々な関数

条件追加（前述のs.add( )）の所には条件式を書きますが、様々な便利な関数も用意されています。下記によく使われる関数を示します。

関数	説明
And	複数の条件を全て満たすかどうか判定
Distinct	全て異なる値を持つかどうか判定
If	If(a,b,c)で、条件aを満たせばb、満たさなければc を返す
Sum	条件式の合計を作成

［参考］z3pyリファレンス

• 複雑な使用例

「5桁の整数で、使われている数字（0～9）が重複するのが多くとも２回まで」

　　例）10242：OK　21100：OK　91959：NG

このように重複をカウントする場合、 Sum ([If( の形式が使われることがあります。なお、○桁の整数を作る方法については、後述の「10桁の整数を生成する例」を参照してください。

（最も重要な部分）
X = [Int("x%d" % i) for i in range(5)]
for a in range(10)):
    s.add(Sum([If(X[k] == a, 1, 0)  for k in range(len(X))]) <= 2)

（参考）全体コードと解説

from z3 import *

X = [Int("x%d" % i) for i in range(5)]

s = Solver()

s.add([And(0 <= X[i], X[i] <= 9) for i in range(len(X))])
s.add(X[0] != 0)
for a in range(10):
    s.add(Sum([If(X[k] == a, 1, 0)  for k in range(len(X))]) <= 2)

r = s.check()
if r == sat:
    result = s.model()
    num_list = [result[d].as_long() for d in X]
    num = int(''.join(str(d) for d in num_list))
    print(num)
else:
    print("解無し")

# 結果出力例
# 21100

［解説］

”Sum ( [ If ( X[k] … “ のところで重複のカウントをしています。重複は２回までOK（Sum(…) <= 2）だが３回以上はNGという条件になっています。

（動作例）

チェックしようとする５桁の整数が21100だった場合、

Xの内容は[ 2, 1, 1, 0, 0 ] となるので、

a=0のとき、 If(X[k] == 0, 1, 0 ) により、[ 0, 0, 0, 1, 1 ] → Sumは 2 → OK　

a=1のとき、 If(X[k] == 1, 1, 0 ) により、[ 0, 1, 1, 0, 0 ] → Sumは 2 → OK

a=2のとき、 If(X[k] == 2, 1, 0 ) により、[ 1, 0, 0, 0, 0 ] → Sumは 1 → OK

a=3のとき、 If(X[k] == 3, 1, 0 ) により、[ 0, 0, 0, 0, 0 ] → Sumは 0 → OK

　　：

a=9のとき、 If(X[k] == 9, 1, 0 ) により、[ 0, 0, 0, 0, 0 ] → Sumは 0 → OK

　全てOKなので、21100でのs.check( ) の結果はsat（条件を満たしている）になります。

（参考）今一つピンとこないという人は、forの部分を下記のようにして表示させてみると良いでしょう。この If(x0 == 0, 1, 0) などの結果（1または0）が並んだリストをSumしているわけです。

for a in range(10):
    print("a=",a)
    print([If(X[k] == a, 1, 0)  for k in range(len(X))])
    s.add(Sum([If(X[k] == a, 1, 0)  for k in range(len(X))]) <= 2)

# a= 0
# [If(x0 == 0, 1, 0), If(x1 == 0, 1, 0), If(x2 == 0, 1, 0), If(x3 == 0, 1, 0), If(x4 == 0, 1, 0)]

5．例

（１）連立方程式の例

変数がごく普通の単純な変数で、リスト（配列）ではないケースです。

以下の連立方程式を満たす解を求めてみましょう。

$$\begin{equation} \left\{ \, \begin{aligned} & 2x+3y=19 \\ & x+4y=22 \\ \end{aligned} \right. \end{equation}$$

from z3 import *

X = Int("x")
Y = Int("y")

s = Solver()

s.add(And(2*X+3*Y==19, X+4*Y==22))

r = s.check()
if r == sat:
    print(s.model())
else:
    print("解無し")


# [y = 5, x = 2]

（２）複数の解を出す方法

問題によっては、複数の解があることもあります。

from z3 import *

x = Int("x")
y = Int("y")

s = Solver()

s.add(x > 0, y > 0)
s.add(x + y == 10)

# 解を探索
while(s.check() == sat):
    # 解の表示
    m = s.model()
    print(m)

    # 解を制約条件に追加
    s.add(Not(And(x == m[x], y == m[y])))

#結果表示（表示順序は異なる場合があります）
# [y = 1, x = 9]
# [x = 1, y = 9]
# [x = 2, y = 8]
# [x = 3, y = 7]
# [x = 4, y = 6]
# [x = 5, y = 5]
# [x = 6, y = 4]
# [x = 7, y = 3]
# [x = 8, y = 2]

［解説］

whileで回しながら、出てきた解を表示したら次々と制約条件に追加していき、同じ解は出ないようにします。

［参考］

PythonでSMTソルバ (z3py) 入門（ochamikan） https://zenn.dev/ochamikan/articles/42ef29b944ed57

（３）10桁の整数を生成する例

変数が1次元のリスト（配列）のケースです。

10桁の整数を生成してみましょう。条件は以下の通りです。

• 10桁の整数を生成します。
• 各桁には0～9の数字をあてはめます。
• ただし、最上位の桁には、０をあてはめることはできません。
• 各桁に当てはめる数字は、どれも異なる数字でなくてはなりません。

from z3 import *

X = [Int("x%s" % i) for i in range(10)]  # [x0, x1,..., x9]

s = Solver()

s.add([And(0 <= X[i], X[i] <= 9) for i in range(10)])
s.add(X[0] != 0)
s.add(Distinct(X))

r = s.check()
if r == sat:
    result = s.model()              # [x9 = 9, x2 = 2, x3 = 3,....]
    num_list = [result[d].as_long() for d in X]     # [1, 0, 2,...]
    num = int(''.join(str(d) for d in num_list))    # 1023456789
    print(num)
else:
    print("解無し")

【応用】※自力でプログラムを改造してもいいし、生成AIを使うのもOKです。

1. このままでは毎回同じ結果になります。乱数を利用して、毎回異なる結果になるようにしましょう。
2. 上記のコードを改造して、10個の異なる10桁の整数が表示されるようにしましょう。

（参考）生成AIを使う場合は、例えば、上記のプログラムをコピペして、「このプログラムでは毎回同じ結果になるので、毎回異なる結果になるようなプログラムにしてください」と追記すればよいでしょう。

（４）魔方陣の例

変数が2次元のリスト（２次元配列）のケースです。

3×3の魔方陣を作ってみましょう。

from z3 import *

X = [[Int("x_%s_%s" % (i, j)) for j in range(3)] for i in range(3)]

s = Solver()
s.add([And(1 <= X[i][j], X[i][j] <= 9) for i in range(3) for j in range(3)])
s.add([Distinct([X[i][j] for i in range(3) for j in range(3)])])
s.add([Sum([X[i][j] for i in range(3)]) == 15 for j in range(3)])
s.add([Sum([X[i][j] for j in range(3)]) == 15 for i in range(3)])
s.add([Sum([X[i][i] for i in range(3)]) == 15])
s.add([Sum([X[i][2-i] for i in range(3)]) == 15])

print(s.check())

m = s.model()
for i in range(3):
    row = []
    for j in range(3):
        row.append(m[X[i][j]])
    print(row)


# 出力結果例
# sat
# [4, 3, 8]
# [9, 5, 1]
# [2, 7, 6]

［解説］

• 1～9の数字での3x3の魔方陣の場合、それぞれの縦・横・斜めの合計は15になることが知られています。上記では、それを利用して簡潔なプログラムにしています。
• ２次元配列の変数Xを作成しています。
• 各マスの数字は、１以上９以下という条件を加えています。
• 各マスの数字は、すべて異なるという条件を加えています。
• それぞれの縦・横・斜めの合計は15になるという条件を加えています。

［出典］

Z3Py　例題　魔方陣（magic square）, @Ganesha, 2021 https://qiita.com/Ganesha/items/fdf965e75f1a49004dd8

【応用】※自力でプログラムを改造してもいいし、生成AIを使うのもOKです。

上記のコードを4×4の魔方陣を作れるように改造してみましょう。さらにn×nの魔方陣はどうでしょうか。AIで生成したらのならばそのプログラムをじっくりと解析して、他の問題に応用できるように理解しておきましょう。

以降はわりと高度な例になります。生成AIや参考ページを利用しながら学んでみてください。

（５）数独の例

数独パズルはZ3の使用例としてネットでよく取り上げられています。いろいろありますので、各自で調べてみてください。

生成AIには「Z3pyを使って数独を解くプログラムを書いて下さい」と質問するといいでしょう。

［参考］

[Python]Z3で数独パズルを解く https://qiita.com/tkinagaki/items/de8c53402f4998177dfd

（６）巡回セールスマン問題の例

巡回セールスマン問題は、複数の都市を全て1回ずつ訪問し、出発地点に戻ってくる最短経路を求める組合せ最適化問題です。

［参考］

Z3Py 例題 巡回問題 https://qiita.com/Ganesha/items/265184b2982f5d80f1fe

（７）スピングラスの基底状態を求める例

３個のイジングスピンが反強磁性的に相互作用していると基底状態は６個あり縮退します。これを算出してみましょう。

なお、「スピングラス」「イジングスピン」などは、イジングモデルや量子コンピューター（アニーリング方式）に関する用語です。各自で調べてみてください。

［参考］

” 量子アニーリングの基礎 ”、西森秀稔・大関真之、2018、共立出版、P.12