2020-05-27

情報科学特別演習の打ち合わせ第2回

状況

英語の文書だが、初学者にとてもやさしい

sat-d の initial commit をした🎉

CNF を表現する DIMACS フォーマットを読み込めるようにした

DPLL を実装した

バグってるので直す。多分すぐに直せる

allClauses に、どの clause にも分類されないような clause が残ってしまっている。

ただ、UNSAT と SAT の判定はちゃんとできている?（$ n = 7 ぐらいの話です……）

↑ 嘘でした。次回の2020-06-03までに解消しました

次回までにやりたいこと

SAT であるときの変数の割り当てが本当に valid であるかを、それらの真偽値を実際に代入することで確認できるようなテストコードを書く /icons/spinner.icon

複数のテストケースをコマンド一つで検証できるようにする /icons/done.icon

minisat で各テストケースが SAT か UNSAT なのかは容易に判定できる。/icons/done.icon

$ apt install minisat でインストールできる