お絵かきロジックの自動解答システムを作る

##お絵かきロジックの複数解チェックを全自動で行いたい

お絵かきロジック（ノノグラム、イラストロジック、ピクロスとも言う）の問題を作ると、
『その問題の解答が必ず1パターンとなっているのかどうか』
のチェックが必要になります。盤面の小さい問題ならともかく、大きい問題ではなかなか骨が折れる作業になります。

この記事は、その複数解チェックをサーバー※にやらせちまおうぜという記事です。
※クライアントでも同じ要領でセットアップをすれば複数解チェックは可能です。

##こんなものが出来上がります

##SATソルバーとは？

SATソルバーとは、「与えられた問題が充足可能（SAT）か、充足不能（UNSAT）かを判定するプログラム」です（参考）。
とてつもなく平たく雑に言ってしまうと、「論理パズル的な問題を解いてくれる（または、解がないことを示してくれる）プログラム」です。
お絵かきロジックだけでなく、数独やナンバーリンク等々のパズルも解くことができる凄いやつです。

この記事では、SATソルバーとして、「Sugar」と「MiniSat」の組み合わせを使用します。

##WebAPIの仕様はこうする
大方針は、**「イラストロジックの問題をJSON形式で渡すと、解が1つの場合にその解を返してくれる。"解なし"か"複数解"だったらそのことを教えてくれる。」**という仕様とします。
手軽にサクッと作りたいので、Python3で書いたプログラムをFlaskで動かすものとします。
これを、以下の仕様に従ったREST APIで実現することにします。

###外部仕様

• 受け付けるHTTPメソッド
  GETとします。

• Bodyパラメーター
  以下のフォーマットのJSONとします。

{
    "Rows" :
        [
            "1行目の数値をアンダースコア区切りで記載",
            "2行目の数値をアンダースコア区切りで記載",
            "（ …中略… ）",
            "最終行の数値をアンダースコア区切りで記載"
        ],
    "Cols" :
        [
            "1列目の数値をアンダースコア区切りで記載",
            "2列目の数値をアンダースコア区切りで記載",
            "（ …中略… ）",
            "最終列の数値をアンダースコア区切りで記載"
        ]
}

↑ 私自身がC#erで、JSONのParserの都合的にパスカルケースだと嬉しいので、パラメーター名を「Rows」「Cols」としています。

###APIの中で行う処理

####1. 受け取った問題の情報（各行・列の制約）を、Sugarが読める形式の制約充足問題（CSP, Constraint Satisfaction Problem）に書き換える。
JSONで渡された各行・列の制約情報を、こちらのサイトで解説されている通りに書き直します。
例えば、

という問題を処理させたい場合、リクエストに積むJSONは以下の内容になります。

{
    "Rows" :
        [
            "3",
            "1_1",
            "2"
        ],
    "Cols" :
        [
            "3",
            "1_1",
            "2"
        ]
}

これをSugarに渡す形式に書き直すと、以下の通りとなります。

(int x_0_0 0 1)
(int x_0_1 0 1)
(int x_0_2 0 1)
(int x_1_0 0 1)
(int x_1_1 0 1)
(int x_1_2 0 1)
(int x_2_0 0 1)
(int x_2_1 0 1)
(int x_2_2 0 1)
(int h_0_0 0 0)
(predicate (r_0 j) (or (and (<= h_0_0 j) (< j (+ h_0_0 3)))))
(iff (= x_0_0 1) (r_0 0))
(iff (= x_0_1 1) (r_0 1))
(iff (= x_0_2 1) (r_0 2))
(int h_1_0 0 2)
(int h_1_1 0 2)
(predicate (r_1 j) (or (and (<= h_1_0 j) (< j (+ h_1_0 1))) (and (<= h_1_1 j) (< j (+ h_1_1 1)))))
(iff (= x_1_0 1) (r_1 0))
(iff (= x_1_1 1) (r_1 1))
(iff (= x_1_2 1) (r_1 2))
(int h_2_0 0 1)
(predicate (r_2 j) (or (and (<= h_2_0 j) (< j (+ h_2_0 2)))))
(iff (= x_2_0 1) (r_2 0))
(iff (= x_2_1 1) (r_2 1))
(iff (= x_2_2 1) (r_2 2))
(int v_0_0 0 0)
(predicate (c_0 j) (or (and (<= v_0_0 j) (< j (+ v_0_0 3)))))
(iff (= x_0_0 1) (c_0 0))
(iff (= x_1_0 1) (c_0 1))
(iff (= x_2_0 1) (c_0 2))
(int v_1_0 0 2)
(int v_1_1 0 2)
(predicate (c_1 j) (or (and (<= v_1_0 j) (< j (+ v_1_0 1))) (and (<= v_1_1 j) (< j (+ v_1_1 1)))))
(iff (= x_0_1 1) (c_1 0))
(iff (= x_1_1 1) (c_1 1))
(iff (= x_2_1 1) (c_1 2))
(int v_2_0 0 1)
(predicate (c_2 j) (or (and (<= v_2_0 j) (< j (+ v_2_0 2)))))
(iff (= x_0_2 1) (c_2 0))
(iff (= x_1_2 1) (c_2 1))
(iff (= x_2_2 1) (c_2 2))
(< (+ h_1_0 1) h_1_1)
(< (+ v_1_0 1) v_1_1)

####2. 処理1で作ったCSPをファイルに書き出す。
Sugarに問題を渡すために、1で作ったCSPをファイルに書き出します。
ファイル名のフォーマットは、「nonogram_%Y.%m.%d.%H.%M.%S.csp」とします。
（例）nonogram_2019.08.20.12.57.40.csp

####3. 処理2で作った問題をSugarに渡し、解かせる。
Pythonのプログラムの中で、Sugarのコマンドを叩きます。
このときの引数で、処理2で作成したファイルを指定します。

####4. 解があった場合は後続処理に進む。解がなかった場合は「Oops! Your question has no answer!」とレスポンスを返して処理を終了する。
処理3で叩いたコマンドの実行結果1行目を参照し、処理を分岐します。
解がある場合は、実行結果の1行目が
s SATISFIABLE
となります。解がない場合は、
s UNSATISFIABLE
となります。

####5. 処理2で作ったCSPファイルの末尾に「今さっきの解答と完全一致しないものとする」という条件を加え、再度Sugarに問題を渡し、解かせる。
先程示した問題を例にすると、「今さっきの解答と完全一致しないものとする」は以下のように書くことができます。

(not (and (= x_0_0 1)(= x_0_1 1)(= x_0_2 1)(= x_1_0 1)(= x_1_1 0)(= x_1_2 1)(= x_2_0 1)(= x_2_1 1)(= x_2_2 0)))

この条件文が実際に意味するところは、
『0行0列のマスがtrue（=黒）かつ0行1列のマスがtrueかつ...(中略)...2行2列のマスがfalse（=白）』という条件と完全一致しないことを解の条件とする
というものです。

####6. 解があった場合は「Oops! Your question has multi answer!」とレスポンスを返す。解がなかった場合は処理4で導出した解を返す。
処理5で解が見つかったということは、問題に少なくとも2つ以上の解があったということを意味します。
その場合には、複数解があることを示すメッセージをレスポンスとして返させます。

処理5で解が見つからなかった場合は、処理3で得た解（唯一解）を返させます。
このとき、黒マスは『#』、白マスは『.』で表現するものとします。

先程示した問題を例にすると、レスポンスとして返す内容は、

###
#.#
##.

となります。

####7. この処理の中で作成したCSPファイルを削除する。
一通りの処理が終わったらCSPファイルは不要となるので、削除します。

##お絵かきロジック解答サーバーの構成

Ubuntu 18.04の上にSugar、MiniSat、Flask（Python3系）をインストールして構築します。
先述の仕様通りに動くPython3のプログラムをFlaskで動かすだけという、構成図も要らないくらいの単純な構成とします。

##環境の構築

まっさらのUbuntu 18.04の上で、以下のコマンドを順次実行していきます。

1. 下準備

1.1. インストール可能なパッケージ一覧を更新する。
sudo apt-get update

1.2. zip解凍ソフトをインストールする。
sudo apt-get install unzip

1.3. JREをインストールする。
sudo apt-get install default-jre

2. MiniSatの導入

2.1. MiniSatをインストールする。
sudo apt-get install minisat

3. Sugarの導入

3.1. Sugarをホームディレクトリ上にダウンロードし、解凍する。
cd ~
wget http://bach.istc.kobe-u.ac.jp/sugar/package/sugar-v2-3-3.zip
unzip sugar-v2-3-3.zip

3.2. Sugarのjarの設置先とするディレクトリを作成し、そこにjarをコピーする。
sudo mkdir /usr/local/lib/sugar
sudo cp ~/sugar-v2-3-3/bin/sugar-v2-3-3.jar /usr/local/lib/sugar/sugar-v2-3-3.jar

3.3. ファイル「（ホームディレクトリ）/sugar-v2-3-3/bin/sugar」をエディタで開き、以下の通りに書き換える。

変更前

my $version = "v2-3-3";
my $java = "java";
my $jar = "/usr/local/lib/sugar/sugar-$version.jar";
my $solver0 = "glucose";
my $solver0_inc = "minisat-inc";
my $tmp = "/tmp/sugar$$";

変更後

my $version = "v2-3-3";
my $java = "java";
my $jar = "/usr/local/lib/sugar/sugar-$version.jar";
my $solver0 = "/usr/bin/minisat";
my $solver0_inc = "minisat-inc";
my $tmp = "/tmp/sugar$$";

3.4. ファイル「（ホームディレクトリ）/sugar-v2-3-3/bin/sugar」を「/usr/bin」に移動し、sugarコマンドを実行可能にする。
sudo cp ~/sugar-v2-3-3/bin/sugar /usr/bin/sugar

4. Flaskの導入

～～～ 注意 ～～～
Pythonの仮想環境上に構築したい場合は、手順を適宜読み替えてください。
この手順では仮想環境を立てずに構築しています。

4.1. Flaskをインストールする。
sudo apt-get install python3-pip
pip3 install flask

4.2. ホームディレクトリ直下に、フォルダ（名前：app）と空のPythonファイル（名前：nonogram_solver.py）を作成する。
mkdir ~/app
touch ~/app/nonogram_solver.py

##お絵かきロジック解答プログラム（nonogram_solver.py）の作成

nonogram_solver.py

from flask import Flask, request
from datetime import datetime
import subprocess
import codecs
import os

app = Flask(__name__)

@app.route("/", methods=["GET"])


def index():

    # Content-TypeがJSONでないリクエストは受け付けない。
    if request.headers['Content-Type'] != 'application/json':
        print(request.headers['Content-Type'])
        return flask.jsonify(res='error'), 400

    #========================================================================
    # JSONに積まれているイラストロジックの行情報と列情報を変数に取得する。
    #========================================================================
    rows = request.json['Rows']
    cols = request.json['Cols']
    row_len = len(rows)
    col_len = len(cols)
    print('Size : ' + str(row_len) + ' * ' + str(col_len))
    print('------------------------------------')

    #========================================================================
    # イラストロジックの問題を、Sugar用の問題文（CSP）に書き換える。
    #========================================================================
    nonogram_csp = ''  # この変数にSugar用の問題文を作り込んでいく。

    for i in range(0, row_len):
        for j in range(0, col_len):
            nonogram_csp += '(int x_' + str(i) + '_' + str(j) + ' 0 1)' + '\n'

    for i in range(0, row_len):
        row_nums = rows[i].split('_')
        for j in range(0, len(row_nums)):
            num = int(row_nums[j])
            nonogram_csp += '(int h_' + str(i) + '_' + str(j) + ' 0 ' + str(col_len - num) + ')' + '\n'

        nonogram_csp += '(predicate (r_' + str(i) + ' j) (or'
        for j in range(0, len(row_nums)):
            num = int(row_nums[j])
            nonogram_csp += ' (and (<= h_'+str(i)+'_'+str(j)+' j) (< j (+ h_'+str(i)+'_'+str(j)+' '+str(num)+')))'
        nonogram_csp += '))' + '\n'
        for j in range(0, col_len):
            nonogram_csp += '(iff (= x_' + str(i) + '_' + str(j) + ' 1) (r_' + str(i) + ' ' + str(j) + '))' + '\n'

    for i in range(0, col_len):
        col_nums = cols[i].split('_')
        for j in range(0, len(col_nums)):
            num = int(col_nums[j])
            nonogram_csp += '(int v_' + str(i) + '_' + str(j) + ' 0 ' + str(row_len - num) + ')' + '\n'

        nonogram_csp += '(predicate (c_' + str(i) + ' j) (or'
        for j in range(0, len(col_nums)):
            num = int(col_nums[j])
            nonogram_csp += ' (and (<= v_'+str(i)+'_'+str(j)+' j) (< j (+ v_'+str(i)+'_'+str(j)+' '+str(num)+')))'
        nonogram_csp += '))' + '\n'
        for j in range(0, row_len):
            nonogram_csp += '(iff (= x_' + str(j) + '_' + str(i) + ' 1) (c_' + str(i) + ' ' + str(j) + '))' + '\n'

    for i in range(0, row_len):
        row_nums = rows[i].split('_')
        for j in range(0, len(row_nums)-1):
            num = int(row_nums[j])
            nonogram_csp += '(< (+ h_' + str(i) + '_' + str(j) + ' ' + str(num) + ') h_' + str(i) + '_' + str(j+1) + ')' + '\n'

    for i in range(0, col_len):
        col_nums = cols[i].split('_')
        for j in range(0, len(col_nums)-1):
            num = int(col_nums[j])
            nonogram_csp += '(< (+ v_' + str(i) + '_' + str(j) + ' ' + str(num) + ') v_' + str(i) + '_' + str(j+1) + ')' + '\n'

    #========================================================================
    # 作ったCSPをファイルに書き出す。
    #========================================================================
    filename = 'nonogram_' + datetime.now().strftime('%Y.%m.%d.%H.%M.%S') + '.csp'
    print(nonogram_csp, file=codecs.open(filename, 'w', 'utf-8'))

    #========================================================================
    # 問題をSugarに渡し、解かせる。
    #========================================================================
    args = ['sugar', './' + filename]
    res = subprocess.check_output(args).decode('utf-8')
    res_rows = res.splitlines()
    res_len = len(res_rows)

    #========================================================================
    # 解があった場合は後続処理に進む。
    # 解がなかった場合は「Oops! Your question has no answer!」とレスポンスを返して処理を終了する。
    #========================================================================
    answer_picture = ''                # 解いた結果の絵をこの変数に収める。
    multi_answer_check_formula = ''    # 複数解有無のチェックを行うためにCSP末尾に追加する条件をこの変数に収める。
    has_multi_answer = False           # 複数解があった場合、この変数をTrueに変更する。

    if 's SATISFIABLE' != res_rows[0]:
        os.remove(filename);
        return 'Oops! Your question has no answer!'

    #========================================================================
    # CSPファイルの末尾に「今さっきの解答と完全一致しないものとする」という条件を加え、
    # 再度Sugarに問題を渡し、解かせる。
    #========================================================================
    row_num = 0
    col_num = 0
    multi_answer_check_formula += '\n' + '(not (and '
    for i in range(1, res_len):
        res_row_parts = res_rows[i].split('_')
        if res_row_parts[0] == 'a x':
            last_val = res_row_parts[2].split('\t')[1]
            if row_num != int(res_row_parts[1]):
                col_num = 0
                answer_picture += '\n'
                row_num = int(res_row_parts[1])
            if int(last_val) == 0:
                multi_answer_check_formula += '(= x_' + str(row_num)  + '_' + str(col_num) + ' 0)'
                answer_picture += '.'
            elif int(last_val) == 1:
                multi_answer_check_formula += '(= x_' + str(row_num)  + '_' + str(col_num) + ' 1)'
                answer_picture += '#'
            col_num += 1
    multi_answer_check_formula += '))'

    print(multi_answer_check_formula, file=codecs.open(filename, 'a', 'utf-8'))
    multicheck_res = subprocess.check_output(args).decode('utf-8')
    multicheck_res_rows = multicheck_res.splitlines()
    if 's SATISFIABLE' == multicheck_res_rows[0]:
        has_multi_answer = True

    os.remove(filename);

    #========================================================================
    # 解があった場合は「Oops! Your question has multi answer!」とレスポンスを返す。
    # 解がなかった場合は、解答の絵を返す。
    #========================================================================
    if has_multi_answer:
        return 'Oops! Your question has multi answer!'
    else:
        print(answer_picture)
        print('------------------------------------')
        return answer_picture


if __name__ == "__main__":
    app.run(host='0.0.0.0')

##実際に動かしてみる

上記のプログラムを作成したら、Flaskを起動します。
python3 ~/app/nonogram_solver.py

起動したら、Postman等のテストツールでサーバー宛てにGETのリクエストを投げます。

唯一解を持つ問題を投げた場合

解がない問題を投げた場合

解が複数ある問題を投げた場合

##課題
問題の行数・列数が多くなると速度面が気になってきます。
以下のようなお膳立てを加えることで計算量を減らして高速化が図れるかもしれませんが、未検証です。

• マス目の白黒を表す変数「x_*_*」が白と黒のどちらになるのかが明らかな場合は、「値が0か1である」という変数定義にせず、初めから固定値にしてしまう。

　　⇒例えば、「列数が20で、とある行の数字が15」となっている場合、その行の真ん中10マスは黒で確定します。
　　　このようにごく簡単にマス目の色を断定できる場合に、「値が1である」という定義にしてしまうことが可能です。

（例）「変数x_2_4の値は1である。」と定義する場合

(int x_2_4 1 1)

##参考にさせていただいたサイト

• お絵かきロジックをSugar制約ソルバーで解く
  http://bach.istc.kobe-u.ac.jp/sugar/puzzles/nonogram.html

• SATソルバーMiniSatとSugarを導入
  https://qiita.com/nt_tn/items/7437a113aa46d23117e4