SATソルバー、ウェブアプリやスマートフォンアプリを作っているような時にはあまり聞かないワードです。コンピュータ科学の理論よりの講義で一回聞いただけという方も多いと思います。というわけで、SATソルバーの説明から行いましょう。
まず、SATソルバーはプログラムです。そしてプログラムですから、入力と出力があります。
SATソルバーの入力は論理式です。論理式は高校数学の意味での論理式そのもので、True/Falseのどちらかが入る論理変数を∧(and)と∨(or)と¬(not)の演算子で組み合わせたものです。
とはいっても大した物ではなくて、プログラマなら慣れ親しんでいるbool式そのものです。例えばC++で書くなら、次のようなもの：
bool p,q,r;
p;
!p;
p && !p;
q || r;
q || ((!q && r) && r);SATソルバーはこのうちの限られたCNFと呼ばれる形のものしか実際には受け取ることができないのですが、これに関してはまたあとで手を動かすときに考えます。
さて、SATソルバーはこれらの入力された論理式を分析して、入力された論理式が「充足できるか否か(SATisfiability)」、さらに充足できるときはその時の論理値表を出力します。具体的には、上の論理式それぞれに対して、次のような答えになります：
p; // yes. p = true;
!p; // yes. p = false;
p && !p; // no. p=trueでもp=falseでも式全体はfalse。
q || r; // yes. q = true または r = true。
q || ((!q && r) && r); //yes. q = true。つまり、変数それぞれにtrue/falseを割り当てた時に、論理式の全体がtrueにできることを「充足できる」とか「充足可能」とかと言います。
3つめはpとしてtrue/falseのどちらを入れても式全体ではfalseにしかなりません。そういう時は「どう頑張ってもこの論理式はtrueにできないぞ」と答えます。この論理式がどうやってもfalseになってしまう論理式は、「恒偽」とか「充足不能」といいます。
あとの２つは、論理式をtrueにする論理変数の割当ての組み合わせがたくさん存在します。たとえば、４つめのq || rはqがtrueならrはtrueでもfalseでも構いません（orですから）。こういう時は、SATソルバーはそのうちの組み合わせのどれか一つを答えてくれます。つまり、
(p,q) = (true,true) or (false,true) or (true,false)のうちのどれかを出力します。
SATソルバーを普通に（？）使うときは論理式で指定された条件さえ満たされて入ればどれでもいい事が多いのですが、今回のようにSATソルバーで計算させる時は結果は一つでなければ困ることが多いです。だって、足し算の結果が２つもあったらこまるでしょう？
SATソルバーに分かるように問題を変換するプログラムをこれから書いていく事になるのですが、そのプログラムのバグで２つ以上充足可能な論理変数の割当てが出てきてしまうことがまれによくあるので、SATソルバーが充足可能だと言った時は、出てきた論理変数の答えの組がちゃんと意図した通りになっているかも確かめながら進めていくとよいでしょう。
今までの説明だと「論理式がTrueになる変数の組み合わせをSATソルバーというソフトウェアが教えてくれるのは分かったけど、だから何なんだ？？」という感想になるのではないでしょうか。
次のChapterでは、簡単な論理パズルを題材に、手を動かしながらSATソルバーで遊んでみます。