ExcelのソルバーをSATソルバーとして使える？ - Qiita結論 とりあえず使える（整数計画問題に直せばよい）。ただし効率がいいかはよく知らない。 はじめに この記事は、私が11月14日に「わんくま同盟 名古屋勉強会#37」で発表した内容の補足記事となります。 取り扱う問題 「SATソルバー」というソフトウェアがある。これは変数を含む論理式（trueとfalseの組み合わせからなる式。演算子としてand, or, notなどを使う）を与えたときに、論理式全体がtrueになるような変数の組み合わせが存在すればそれを一つ返し、なければ「組み合わせは存在しない」と答えてくれるものである。 例えば数独のような「所定の枠が存在して値を埋めていく（決定すべき値の数が有限である）タイプのパズル」を、適切な論理式で書くことで、あとは自動的に解かせるということも可能である（論理式が膨大になるケースもあるので、適切な時間で解けるとは限らない）。上記発表での発表資料で概
