# 今年やったこと
アドカレの存在を忘れていて気づいたら自分の番が過ぎてました。ひっそりと公開しておきます。この記事は[法政大学 Advent Calendar]( https://adventar.org/calendars/6528)13日目の記事です。

こんにちは kanadeです。最近Aespaがマイブームです。MAMAの新人賞も受賞して勢いがどんどん増してますよね。ちなみにMAMAの受賞者見ていたらAdoさんがいてびっくりしました。日本枠というのがあるんですね。

今年もいろいろなことがありました。研究したりインターンしたりバイトでコード書いたり、昨年よりも関わるコミュニティが増えて充実したいい意味でとても忙しい一年でした。
それらに加えて今年の夏にはセキュリティキャンプ・ネクストに参加しました。恒例の参加記とか課題晒しみたいなのをやろうかなと考えていたらもう今年も終わり、、、ということで、その中から一つのネタを書こうかなと思います。

## 概要
キャンプの講義は1講義につきだいたいが2コマあり、1回目にインプット、2回目には1回目を踏まえた独自のアウトプットを行う形式となっています。基本的には自分のアイディアを実装して発表するという形式でした。研究では機械学習と画像処理、自然言語処理あたりをやっているのでその辺と絡めて何かやりたいと考えていました。

特にそれがハマったのが形式手法を学ぶ講義でした。形式手法とは大雑把に言うと、数理論理学を使いプログラムの正しさを検査する手法です。
大学ではこのような授業はとってこなかったので（あるかどうか不明）完全に初めてでしたが周りの受講生を見ていると講義で扱ったという人が多かったです。
ちなみに半分ぐらいの受講者が[TAPL](https://www.amazon.co.jp/dp/B07CBB69SS)を読んでいて焦りました。聞いてみると大学の技術系サークルなどでTAPLの輪読会が開かれたりしているみたいですね。[IEEE Xplore](https://ieeexplore.ieee.org/book/6267321)を開けば弊学の人もタダで読めるのでぜひどうぞ。

授業ではホーア論理や型付きラムダ計算など慣れない言葉が多く登場し、それら何かを使ったアプリケーションを作成する課題が出ました。しかし、自分自身この分野にまったく触れて来ませんでした。そのため、他の人にも何か触れるきっかけになるような面白いものを作りたいという動機が生まれ、それをテーマに作ってみました。

## 作ったもの
SMTソルバを使って数独を解く！というものです。SMTソルバとは述語論理を扱い、充足可能であるかを判定するもので、その応用としてプログラム検証などが挙げられます。例えばxとyが整数の変数であるとき
$$
x>y \quad \lor \quad x<2
$$
のような式が与えられて、$$x=0　y=1$$のように式を満たす（充足可能である）ものを探すのがSMTソルバです。
この「SMTソルバを使って数独を解く」というのは実は先人たちがN回とやってきています。しかもこの[SMTソルバの自作](https://rkx1209.hatenablog.com/entry/2017/12/17/175439)までやっている方もおり(有名な方ですね)なかなかオリジナリティを発揮できなさそうでした。そこでいろいろと考えました。これのめんどくさいところは、数独の盤面を全部プログラムに入力しないといけない点です。9x9の盤面だったら二次元の配列に81マス分の数字を埋めなければいけないわけで手間がかかります。ものぐさな自分は、じゃあ数独サイトの画像を入力して遊べれば面白いんじゃ？？と考え、実装してみることにしました。

## やりたいこと
上のような数独の画像を入力すると解答を自動的に作ってくれるものを作ります。画像は適当に数独サイトからスクショして持って来ます。
## 手順
### 画像の前処理
数独の画像は基本的に罫線が入っているため文字認識したときに邪魔になりそうです。なので除去しておきましょう。ImageMagickを使用します。

convert $1 -type Grayscale -negate -define morphology:compose=darken -morphology Thinning 'Rectangle:1x60+0+0<' -negate out.png

このコードを実行すると、、、

綺麗サッパリ罫線の除去が行えました! これで文字認識もいけそうですね！

### 文字認識
画像中の文字を認識します。OCRです。これはGoogleのCloud Vision APIを利用します。
ここで先ほどの前処理がある場合とない場合の文字認識能力の違いについてみてみましょう。
左が罫線除去なしで右側が罫線除去ありです。左では中心の1などの3か所の数字が認識されていませんが、罫線を除去することで全部の数字を検知することができました。
### プログラム上で扱えるようにする
数字が無事に読み込めたらあとはそれを二次元の配列に直してプログラム上で扱えるようにするだけです。Cloud Vision API では文字のバウンディングボックスの座標を取得することが出来ます。幸い、今回扱う数独の画像は基本的に正方形に近い形で、NxNマスの配置が規則的に碁盤の目状に並んでいるため、どのマスに数字があるかの判定が楽に行えます。やり方としてはバウンディングボックスの4点の座標をx,y座標それぞれ取得して平均をとり、その値を画像のheight及びwidthで割り、行数及び列数を乗算するいった流れです。今回は9x9なのでx,yともに9ですね。このロジックで何行何列にどの数字が格納されるかがわかります。例えば、最も左に位置する「9」は3行1列目にありますね。この3と1を求めることが出来ます(コード上は0-indexなので2,0) コードを抜粋するとこんな感じです。

height = res_json['fullTextAnnotation']['pages'][0]['height']
width = res_json['fullTextAnnotation']['pages'][0]['width']
blocks = res_json['fullTextAnnotation']['pages'][0]['blocks']
for block in blocks:
    words = block['paragraphs'][0]['words']
    for word in words:
        for symbol in word['symbols']:
            text = symbol['text']
            vertices = symbol['boundingBox']['vertices']
            x,y = 0,0
            for vertic in vertices:
                x += vertic['x']
                y += vertic['y']
            x = x//4
            y = y//4
            x_location = int(x / width * 9) 
            y_location = int(y / height * 9)
            print(f"value:{text}, row:{y_location}, col:{x_location}")
            array[y_location][x_location] = int(text)

このy_locationとx_locationに0~9の行数列数が入ります。jsonが複雑で大変ですが一歩ずつ頑張りました。
### ソルバで解く
ここは他の方が詳しく書かれていると思うので特に詳しくは述べません。気になる方は「SATソルバ　数独」で調べてください。
数独なので今回満たす制約は以下の3つです。
- 一行に0~9が一つずつ被らないように入れる
- 一列に0~9が一つずつ被らないように入れる
- 大きい枠で囲われたマスに0~9が一つずつ被らないように入れる

この制約を満たすCNFが実装できたら準備完了です。

### 結果
さて、ドキドキの結果です。
画像のみの入力で数独を解くことが出来ました。右の図を見てもおかしいところはありません！やったね！！

### 感想
本当は結果だけを無機質にコンソールに出力するだけでなく、解答の画像を生成するところまで持っていきたかったです。フロントエンドを作って数独解く君というWebアプリにしたかったのですがそこまでの時間はなかったです。落ち着いたら続きを作ろうかなと思います。

### まとめ
自分の専門分野と他の分野を絡めて何かやってみるのは面白いですね。この他にも計算式をOCRで文字起こしして得られた式を自作の構文解析機に入力してみたりなど、他にも色々楽しそうなことが見つかります。この分野とまじめに機械学習を絡めるならAIファジングとかそういう方向になると思いますが、ちょっと視点を変えて遊んでみるのも面白いです。

### さいごに
今年も楽しいことが出来ました。来年もまた色々チャレンジしていきます。Aespaのようにエネルギッシュに色々なことができるといいな。