TL;DR

ゴミ記事なので本当に読まなくていいです.

はじめに

LAWSON presents 麻倉もも Live Tour 2022 “Piacere!” の開催に際して, 全10問のそこそこムズい4択クイズをやることになりました.

trysail.jp

初日に真面目にやったら正解数は2問でした. それから数日間それなりにちゃんと考えつつ挑戦しましたが, 7問正解から伸びることはなく, 筆者は麻倉ももさんを理解できていないと痛感しました.

麻倉ももマスターへの道のりは遠いですが, 筆者はコンピュータサイエンスでマスターを取っているので, コンピュータに仕事をさせることにしました.

本当はこれを TL;DR に書くべき

4択クイズへの回答と正解数を制約条件とした制約充足問題を定式化し, SAT ソルバを用いて解く事で正解を導いた.

制約充足問題 (CSP) とは？

~~自分の修論に書いてるから引用するのが楽だなと思いつつ~~

制約充足問題 - 数理計画用語集

こんな感じ. 要はいくつかの変数からなる等式とか不等式とかを全て満たすように変数に値を割り当てられるか判定する問題.

例) 整数変数 $x,\ y \in \mathbb{Z} ,\ -10 \leq x,\ y \leq 10$ について, 次の制約式

${\displaystyle \begin{eqnarray} \left\{ \begin{array}{l} x + y = 3 \\ x^{2} + x - 6 = 0 \end{array} \right. \end{eqnarray} }$

を満たす値は存在するか？答えは Yes である ( $\lbrace x,\ y\rbrace = \lbrace -3,\ 6\rbrace,\ \lbrace 2,\ 1\rbrace$ ).

充足可能性問題 (SAT) とは？

充足可能性問題 - Wikipedia

かなーりめちゃくちゃ雑に言えば2進数の変数に限定した制約充足問題である.

雑に全探索すると $n$ 個の変数と $m$ 個の制約式からなる SAT 問題は $O(2^{n}mn)$ 回の探索が必要となるが, この世の中にはもっと高速に解を探索するソルバがいっぱい存在する.

https://jssst-ppl.org/workshop/2017/slides/ppl2017_c4_soh.pdf

使用ツール

制約充足ソルバとして Sugar を用いる.

cspsat.gitlab.io

Sugar は与えられた CSP を SAT にエンコードし, SAT ソルバで解を求め, 解が存在する場合は元の問題の解にデコードするソルバである.

上記の例の問題を Sugar CSP で記述すると以下の通りとなる.

(int x -10 10)
(int y -10 10)
(eq (+ x y) 3)
(eq (+ (* x x) x -6) 0)

実行してみるとこんな感じ.

[f_t_ikt]:$ cat >ex.csp
(int x -10 10)
(int y -10 10)
(eq (+ x y) 3)
(eq (+ (* x x) x -6) 0)
[f_t_ikt]:$ sugar ex.csp
s SATISFIABLE
a x     2
a y     1
a

注意すべきなのは, SAT ソルバは「制約を充足する値の割当てが存在するか否か」を判定するものであり, 上記の例のように複数通りの解が存在するとしてもすべての解を求めるわけではない.

また, SAT ソルバは MiniSat を用いる.

MiniSat Page

いないと思うけど試してみたい方には以下の記事が参考になる.

SATソルバーMiniSatとSugarを導入 - Qiita

余談だが, 筆者は学生時代にある問題の解が存在しないことを証明するために, 様々な SAT ソルバを試して悪戦苦闘していた.

定式化してみる

そういうわけなので, 変数と制約式を定義すれば解ける！簡単！

① 各問題の選択肢に対応する変数を定義する.

クイズの問題数を $N = 10$ , 選択肢の数を $M = 4$ とする.

${\displaystyle x_{i,\ j} = \begin{eqnarray} \left\{ \begin{array}{l} 1\ \ {\rm{if}}\ i\ 番目の問題の\ j\ 番目の選択肢が正解である\\ 0\ \ \rm{otherwise} \end{array} \right. \end{eqnarray} }$

${\rm{for}}\ i \in \lbrace 1,\ 2,\ \dots\ ,\ N\rbrace,\ j \in \lbrace 1,\ 2,\ \dots\ , M\rbrace$

② 「選択肢は各問題で1つのみが正解となる」という制約を追加.

$\displaystyle \bigwedge^{N}_{i = 1}\left(\sum^{M}_{j = 1} x_{i, j} = 1\right)$

③ 制約式を定義するためにクイズに~~適当に~~答え, 解答内容と正解数をメモる.

より確実に絞り込むために, 全部1番目のとき, 2番目のとき, 3番目のときの正解数も調べておいた. つまりこれで3日消費している.

④ いい感じに溜まってきたら制約式をドーンと追加.

クイズに挑戦した回数を $T$ とする ( $T=19$ らしい).

$c_{t,\ i} = (t\ 回目の挑戦時に\ i\ 番目の問題で選んだ選択肢)$

$a_{t} = (t\ 回目の挑戦時の正解数)$

${\rm{for}}\ t \in \lbrace 1,\ 2,\ \dots,\ T\rbrace$

として, 以下の制約を追加.

$\displaystyle \bigwedge^{T}_{t = 1} \left(\sum^{N}_{i=1} x_{i,\ c_{t,\ i}} = a_{t}\right)$

式で書くと何だこれと思うような見た目だが, 要はすべての試行に対して, 選んだ選択肢で何問正解したかということを表現しているだけ. 各変数に0か1を割り当てて矛盾が生じなければ, 1となった変数に対応する選択肢が正解となる, かもしれない.

こんだけ？はい.

⑤ Sugar CSP で記述して解かせる.

手で書くのはめんどくさいので, 退屈なことはPython にやらせよう.

for i in range(1,11):
    for j in range(1,5):
        print(f"(int x_{i}_{j} 0 1)")
        
for i in range(1,11):
    print("(eq (+",end="")
    for j in range(1,5):
        print(f" x_{i}_{j}",end="")
    print(") 1)")

while True:
    s = []
    try:
        s = input().split()
    except:
        break
    print("(eq (+",end="")
    for i in range(10):
        print(f" x_{i+1}_{s[i]}",end="")
    print(f") {s[-1]})")

あとは任せた！ 1秒ほどで Sugar くん (というか MiniSat くん) がゴリゴリに探索してそれっぽい解を吐き出す.

⑥ 麻倉ももマスターの称号を手に入れる.

頭を使わないために頭を使うのが好きです. これは使ったうちには入りません.

アホ

あろうことか福岡公演の日にメモを取り間違えて一生 UNSAT を吐き続けていた. メモも取れないしクイズもできないアホと申します.

まとめ

4択クイズの解答状況を制約として, CSP を定式化し, SAT ソルバを用いて解く方法を提案した. 筆者の解答状況にはばらつきがあったからか, 無事に正解となる一意解を出すことに成功した.

考察

麻倉ももさんかわいい.

むすびに

これ全然学部レベルです.

よくない言葉集

よくない言葉を連ねます。日本語が不自由なので閲覧非推奨です。

修士 (工学) なので計算機でパワープレイして修士 (麻倉もも) になった話