SATソルバを使うためにCNFを作る - soutaroブログ
SATソルバっていうのは，充足可能性問題（SATisfiability problem）を解いてくれるソフトウェアのことで，SATソルバで数独を解くとか，以外と身近なところに応用があったりします．SATソルバは数独を解くだけじゃなくて，プログラムの停止性の判定に使うとか，いろいろな応用を考えることができる良いものです．普通，SATソルバはCNFという論理式の特殊な形を取り扱います．日本語だと乗法標準形とか言うらしいですけど，別にこの言葉は忘れても良いと思います．詳しくはWikipediaでも見てもらえれば良いのですが，CNFは，変数かそのnot付けたやつ，をorで結んだやつ，をandで結んだやつ，という意味です． CNF ::= c1 && ... && c2 c ::= l1 || ... || l2 l ::= x | !x 任意の論理式(変数(x)とor(||)とand(&&)と「な
Publication: A Pearl on SAT Solving in Prolog - School of Computing - University of Kent
Jacob M. Howe and Andy King In Matthias Blume and German Vidal, editors, Tenth International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, April 2010. Abstract A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solv
SATsolver - ここに何かをWiki
DeductionAlgorithm（パワポ） DPLL 卒論キックオフ資料 PDF PPT ネタ･メモをつらつら書いていこう。 意義 以下の応用分野に適用できるSATソルバだが、SAT問題はNP完全問題である。何も工夫せずに解こうとすると（総当り）、2のn乗という指数的コストがかかってしまう。要素数がちょっと増えただけで使い物にならなくなってしまうわけだ。SATソルバの大きな目的として、この探索域の削減が挙げられる。調べる必要が無くなった探索域は、ばっさり切り捨ててしまうのだ。 SATソルバは長年研究が成されていて、最近はDPLLベースのアルゴリズムに落ち着いているらしい。しかしながら、SATCompetitionという大会があるのだが、そこで1位になるようなSATソルバでも制限時間内に解けない問題が沢山ある。まだまだSAT問題は速く解くことが求められている分野だと言えよう。 また、並列
SAT Live!
Recent news about SAT subscribe via RSS Jan 18, 2024 SAT 2024 Call for Workshops by Alexey Ignatiev SAT CFW Deadline 27th International Conference on Theory and Applications of Satisfiability Testing Dec 10, 2023 Tenure-track assistant professorship in foundations of computer science with a focus on logic and automated reasoning (application deadline Jan 26) by Jakob Nordström Position Deadline Th
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
SAT Solvers A Brief Introduction
SAT Competitions