SATを用いた解法

摘要

配線問題は，マスとマスを結ぶ線を「引く」か「引かない」かという0/1の判断の結果が正しい解となっているかを判定する問題とみなせるので，比較的単純にSAT問題に定式化することができる. SATとはSAT is fiabilityの略であり，通常は「充 足可能性」と訳される.多くの場合，命題論理式 の充足可能性判定問題をSAT問題と呼び，SAT 問題を解くプログラムのことをSATソルバーと呼 ぶ.コンピュータ科学の視点から見ると，SAT問 題はNP完全問題であることが知られており，現 時点では問題のサイズに対して多項式時間で解ける ことを保証したアルゴリズムは存在しない.しかし， SAT問題を解く効率の良いアルゴリズムの研究は 非常に活発に行われており，特に今世紀に入ってか らの性能向上は目覚ましいものがある.