はじめに

前回は地獄のSMT-LIBコピペ祭りを経て、z3で数独を解くことに成功しました。今回はVBから制約を発行してz3に数独を解かせてみましょう。

.NETバインディング

z3には.NETのバインディングが用意されており、P/Invoke祭りやCOM祭りをやらなくともz3の機能が利用できます。やったね

まぁ、CodeDOMからコードを生成するのによく似たつらみが待ち構えているので結局アレですけど。

z3のGitHubページからライブラリをダウンロードして、Microsoft.Z3.dllを参照に加えましょう。また、Microsft.Z3.dllは単なるバインディングなので、libz3.dllも一緒にコピーしておく必要があります。

あと、libz3は（たぶん）ネイティブなので、ダウンロードしたアーキテクチャに合わせて.NETのアーキテクチャを合わせておく必要があります。 WOW64の加護により64bitOSでも32bitアプリケーションが動くので今回はx86を使用しています。アプリケーションに割り当て可能なメモリ量の制約や若干のオーバーヘッドなどがありますが、今回は目をつぶりましょう。

余談ですが、x86のネイティブライブラリを使用しているプロジェクトで、Debugビルドはx86に直してあるのにReleaseはAnyCPUのままになっていてReleaseすると無事に64bitOSで死ぬみたいな間抜けな事があったので気を付けましょう。

数独

正直なことを申しますと、z3の公式サンプルに数独を解くコードがあるのでそちらを参考にしました。

Dim opt = New Dictionary(Of String, String)
opt("proof") = "true"

Using c = New Context(opt)
    Dim solver = c.MkSolver()

    Dim cells(8)() As IntExpr

    ' x_1_1 から x_9_9のシンボルを生成
    For i = 0 To 8
        Dim r(8) As IntExpr
        cells(i) = r

        For j = 0 To 8
            cells(i)(j) = CType(c.MkConst(c.MkSymbol($"x_{i + 1}_{j + 1}"), c.IntSort), IntExpr)
        Next
    Next

    ' (assert (and (<= 1, x_?_?) (>= x_?_? 9)))
    For i = 0 To 8
        For j = 0 To 8
            solver.Assert(
                c.MkAnd(
                    c.MkLe(c.MkInt(1), cells(i)(j)),
                    c.MkLe(cells(i)(j), c.MkInt(9))))
        Next
    Next

    ' (assert (distinct x_?_1 ... x_?_9))
    For i = 0 To 8
        solver.Assert(c.MkDistinct(cells(i)))
    Next

    ' (assert (distinct x_1_? ... x_9_?))
    For j = 0 To 8
        Dim col(8) As IntExpr
        For i = 0 To 8
            col(i) = cells(i)(j)
        Next

        solver.Assert(c.MkDistinct(col))
    Next

    ' (assert (distinct 3x3のあのマス))
    For i0 = 0 To 2
        For j0 = 0 To 2
            Dim square(8) As IntExpr

            For i = 0 To 2
                For j = 0 To 2
                    square(3 * i + j) = cells(3 * i0 + i)(3 * j0 + j)
                Next
            Next
            solver.Assert(c.MkDistinct(square))
        Next
    Next

    Dim inst =
    {
        {0, 0, 5, 3, 0, 0, 0, 0, 0},
        {8, 0, 0, 0, 0, 0, 0, 2, 0},
        {0, 7, 0, 0, 1, 0, 5, 0, 0},
        {4, 0, 0, 0, 0, 5, 3, 0, 0},
        {0, 1, 0, 0, 7, 0, 0, 0, 6},
        {0, 0, 3, 2, 0, 0, 0, 8, 0},
        {0, 6, 0, 5, 0, 0, 0, 0, 9},
        {0, 0, 4, 0, 0, 0, 0, 3, 0},
        {0, 0, 0, 0, 0, 9, 7, 0, 0}
    }

    For i = 0 To 8
        For j = 0 To 8
            If inst(i, j) <> 0 Then
                solver.Assert(c.MkEq(c.MkInt(inst(i, j)), cells(i)(j)))
            End If
        Next
    Next

    If solver.Check() = Status.SATISFIABLE Then
        Dim m = solver.Model

        For Each i In cells
            For Each j In i
                Console.Write($"{m.Evaluate(j)} ")
            Next
            Console.WriteLine()
        Next
    Else
        Console.WriteLine("Failed to solve sudoku")
    End If

End Using

おわりに

z3で数独を解くこと自体は前回の時点で出来てるので今回は特に感動もないのですが、まぁなるほどなといった感じです。しかしまぁ、慣れは必要ですが問題を数式で表現さえ出来ればアルゴリズムを実装せずに解けるというのはかなり強力ですね。

公式サンプルではほとんどの制約を(and ...)で連結してAssertを2つにまで削減してました。内部実装的にこうしたほうが早いというのがあるのかもしれませんが、今回は分かりやすさの為に条件一つ一つにAssertを適用しました。

github.com

おわり

レンコン畑でつかまえて

VB.NETでも制約ソルバーを用いて数独を解きたい　その２

はじめに

.NETバインディング

数独

おわりに