2020-10-14

情報科学類誌「WORD」で SAT ソルバーの記事を書くことになったので、途中まで書いた原稿を先生に添削していただいた

命題論理の充足可能性問題と書くと曖昧さが弱まる

propositional sat

A, B, C が命題変数を表していることを明記したほうが良い

変数, メタ変数

メタ変数 …… 論理式を表すメタ変数 など

普通の変数 …… 命題論理式を構成する変数

これらを区別するべき

UNSAT のとき、sat competition では矛盾であることの証明を出力することを要求している

一般的な solver は SAT であるときの変数の割り当てを出力しているが、これは必要であるというわけではない

Tseytin 変換について

equi-sat に変換する

CNF の簡約化

日本語における定訳があるかもしれない（単純化というのもあるかも？）

DPLL での、単位伝播できないときの変数の割り当てについての説明がない

単位節についての説明もない

DPLL の基本動作について

未割り当ての変数について真偽を割り当て、全ての節が削除される or 空節が現れるまで割り当てを繰り返す

空節が生まれたら充足できないので別の割り当てを試す（backtrack）

DPLL の高速化ポイント

空節が出たときにすぐ backtrack

単位伝播によって枝刈りが行われる

これらがもっとわかりやすく書かれると良い

疑似コード

ρ の意味をどこかで書く

ρ がリテラルの集合のような

ρ ∪ {l} がリテラル l に True を assign する

「ρ で割り当てられていないリテラル」の曖昧

x が True であるとき ¬x は割り当てられていないリテラルであるが……

x が割り当てられていないとき x と ¬x のどっちを取るのか？

conflict

DPLL では空節が出るような割り当て（x, ¬x）をした状況のことを conflict と呼ぶ

空節と conflict の対応を取りつつ説明……