SATソルバ
SATソルバ
SAT(boolean SATisfiability problem)
充足可能性問題
与えられた命題論理式を真にする値割り当てが存在するか否かを判定する問題
→SAT問題
SATソルバは、与えられたSAT問題が充足可能 (SAT) か充足不能 (UNSAT) かを判定するプログラム
NP問題のNP完全である問題であると最初に証明されたもの
充足問題の例
パズル
数独
8クイーン
スケジューリング問題
グラフ彩色問題
魔方陣
お絵かきロジック
連言標準形(CNF)
DIMACS CNF
DIMACS Format
MiniSat (C++)
picosat (C)
SAT4J (Java)
SAT ソルバーの最新動向と利用技術
SATソルバの競技大会があってそれでどんどん向上しているらしい
SAT Competition
SATRace
SAT Challenge
本
The Art of Computer Programming
Handbook of Satis ability
確認用
Q. SATソルバ
Q. 充足可能
Q. 充足不能
Q. SAT
Q. UNSAT
参考
SATソルバーとソフトウェア検証技術(その1) - IDAJ-BLOG
2017/03/09
SAT ソルバーの最新動向と利用技術
2022/02/24
事前に問題を検出できる仕組み SATソルバとSMTソルバによる充足可能性判定 - ログミーTech
充足可能性問題 - Wikipedia
2022/10/13
SATソルバの紹介
関連
モデル検査
SMTソルバ
SAT問題
探索アルゴリズム