2020-10-28
引き続き、記事の添削をした。
DPLL アルゴリズムのところで用語の説明が入っている。
2章のところで CNF の説明も入れてしまったほうが良いのかもしれない、それは DPLL でも CDCL でも共通のことであるため
「DPLL や CDCL でも CNF を利用している」という旨を入れてあげるとわかりやすいかもしれない
基本的には、セクションのタイトルに対応した内容が来ることが期待されるので、SAT の問題形式や用語の定義に対応する CNF を DPLL のところに入れてくるのは適切でないかもしれない。
そのアルゴリズムでしか利用されないような用語を、そこの最初に説明するのは良さそうだが……
CNF、単位節、
「DPLL の肝」で全体の説明になり、CNF の単純化は sub procedure っぽい
トップダウンな説明にしたほうがわかりやすいかもしれないので、順序が逆のほうが良い
「このとき、与えられた……ということになります。」は SAT ソルバーの話である……
これを DPLL の肝のところに持ってきて、CNF の単純化をその後に持ってくると良い流れになるかもしれない。
3節の冒頭(subsection の前)として DPLL の肝を入れてもいいのかも?
「前者の場合は……」でパラグラフが分かれているのは変かも
SAT ならそこで動作を終わりにして良いということを書く
衝突
DPLL でも CDCL でも同じ
衝突の直前に l, not l が割り当てられたことによって〜……と書いておくと良いのではないか
違う経路で枝刈りがなされる可能性があるということ
Backtrack が何をするのかとか、Deduce が何をするのかの説明がほしい(疑似コードがざっくりとしすぎているため)
問題の実行例のようなものを出すと追いやすいかもしれない(図に関して)
それなりの大きさの例を一定して説明に利用してあるとわかりやすさが向上する
SAT ソルバーの応用についてもやってみたいという話(数独を例に挙げた)
後で読む
quantified Boolean formula problem (QBF) のことについて触れていたら、詰将棋の話が出てきた(名古屋大の木原 貴行先生の YouTube の動画について)