SAT booleanな充足可能問題. 拡張したものに SMT がある. SAT Solver 今どきのSAT solverは基本に DPLLアルゴリズム - Wikipedia が用いられているらしい . SAT符号化 watchlater 読もう