始めに

みなさん、中学生の時に数学の授業でグラフを描いたことありますよね？
例えば$y=x^2$のグラフは放物線になります。そしてこんなことも考えたはずです。

適当に線を描いたら、それを表す関数が作れるんじゃないの？

と。つまり数式からグラフを導き出すのではなく、グラフから数式を導き出そうということです。
そんな夢のようなことをしてみたかったなぁ、という記事です。

方針

Pythonで実装します。主に使用するライブラリは以下の2つです。

ライブラリ	用途
Tkinter	線を描くためのキャンバスを生成するために使用します。
Z3	与えられた数学的条件を満たす解を得るために用いる、Microsoft製のライブラリです。

Tkinterで描いた線の通った座標$(x, y)$を満たすべき条件に使用し、Z3で解を求めます。

実装

クラス名	役割
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の存在を知って、昔感じた疑問を検証してみようと思ったのですが、現実は甘くありませんでした。
もっと便利なツールがあるのかな？