始めに
みなさん、中学生の時に数学の授業でグラフを描いたことありますよね？
例えば$y=x^2$のグラフは放物線になります。そしてこんなことも考えたはずです。
適当に線を描いたら、それを表す関数が作れるんじゃないの？
と。つまり数式からグラフを導き出すのではなく、グラフから数式を導き出そうということです。
そんな夢のようなことをしてみたかったなぁ、という記事です。
方針
Pythonで実装します。主に使用するライブラリは以下の2つです。
| ライブラリ | 用途 |
|---|---|
| Tkinter | 線を描くためのキャンバスを生成するために使用します。 |
| Z3 | 与えられた数学的条件を満たす解を得るために用いる、Microsoft製のライブラリです。 |
実装
| クラス名 | 役割 |
|---|---|
| Main | エントリーポイントです。 |
| IPaintListener | 描画時に呼ばれる関数を宣言したインターフェースです。 |
| Paint | ペイントツールのようなキャンバスを生成し、ここに線を描いていきます。キャンバスを操作した時にIPaintListenerへ通知を送ります。 |
| SMT | 解となる数式を求めます。 |
ソースコードは以下の通りです。折り畳んでいます。
なお、Paintクラスを実装するにあたって、Tkinterでペイントもどきを作るを参考にしました。
折り畳んでいます
Main.py
from Paint import Paint
from SMT import SMT
if __name__ == '__main__':
# インスタンスを生成
paint = Paint()
smt = SMT()
# マウス操作のリスナーを登録
paint.set_listener(smt)
# メイン処理開始
paint.start()
IPaintListener.py
from abc import ABCMeta, abstractmethod
class IPaintListener(metaclass = ABCMeta):
# 左クリック時に呼ばれる
def on_click(self, x, y):
return
# ドラッグ実行時に呼ばれる
def on_drag(self, x, y):
return
# リセット時に呼ばれる
def on_reset(self):
return
# 完成時に呼ばれる
def on_complete(self):
return
Paint.py
import tkinter
from IPaintListener import IPaintListener
class Paint:
def __init__(self):
# 描画中の線のIDを初期化
self.current_id = -1
# メインウインドウを作成
self.root = tkinter.Tk()
self.root.title("Paint")
# リセットボタンを作成
reset_button = tkinter.Button(self.root)
reset_button.config(text = "リセット", command = self.on_reset)
reset_button.pack()
# 完成ボタンを作成
complete_button = tkinter.Button(self.root)
complete_button.config(text = "完成", command = self.on_complete)
complete_button.pack()
# キャンバスを作成
self.width = 200
self.height = 200
self.canvas = tkinter.Canvas(
self.root, width = self.width, height = self.height, bg = "white")
self.canvas.pack(expand = True, fill = tkinter.BOTH)
# 描画処理を登録
self.canvas.bind("<ButtonPress-1>", self.on_click)
self.canvas.bind("<B1-Motion>", self.on_drag)
# リスナーを初期化
self.listener = None
# メインループ開始
def start(self):
self.root.mainloop()
# リスナーを登録
def set_listener(self, listener: IPaintListener):
self.listener = listener
# 左クリック時に呼ばれる
def on_click(self, event):
self.current_id = self.canvas.create_line(
event.x, event.y, event.x, event.y, fill = "black", width = 1, tag = "line")
if self.listener is not None:
self.listener.on_click(event.x, event.y)
# ドラッグ実行時に呼ばれる
def on_drag(self, event):
points = self.canvas.coords(self.current_id)
points.extend([event.x, event.y])
self.canvas.coords(self.current_id, points)
if self.listener is not None:
self.listener.on_drag(event.x, event.y)
# リセット時に呼ばれる
def on_reset(self):
self.canvas.delete("line")
if self.listener is not None:
self.listener.on_reset()
# 完成時に呼ばれる
def on_complete(self):
if self.listener is not None:
self.listener.on_complete()
SMT.py
from z3 import *
from IPaintListener import IPaintListener
class SMT(IPaintListener):
def __init__(self):
self.f = Function("f", RealSort(), RealSort())
self.s = Solver()
# 制約を追加
def add_constraint(self, x, y):
self.s.add(self.f(x) == y)
# 解を求める
def solve(self):
result = self.s.check()
print(result)
if result == sat:
print(self.s.model())
# 左クリック時に呼ばれる
def on_click(self, x, y):
self.add_constraint(x, y)
# ドラッグ実行時に呼ばれる
def on_drag(self, x, y):
self.add_constraint(x, y)
# リセット時に呼ばれる
def on_reset(self):
self.s.reset()
# 完成時に呼ばれる
def on_complete(self):
self.solve()
結果
こんな感じのツールが出来上がりました。完成ボタンを押すことで数式を求めます。
しかしタイトルを読んで察しているかと思いますが、全然上手くいきませんでした。
適当な線を描いてみたら充足不可能になるか、充足可能でも単に条件の数だけ分岐のある関数ができるだけで、中学生の時に勉強した多項式はできませんでした。
座標$(x, y)$から上手く制約条件を設定できればいいんですけど、まだまだ勉強不足です。
最後に
お盆休みの間に勉強していたらSMTソルバやZ3の存在を知って、昔感じた疑問を検証してみようと思ったのですが、現実は甘くありませんでした。
もっと便利なツールがあるのかな？