SATソルバーを動かすときには，論理式をCNFで与えなければならない．初めからうまく書ければ良いが，ただでさえ論理式を作るのは面倒なので，論理式自体は普通に書いておいて，あとからCNFに変換した方が考えやすい．分配則を使って変換すると，論理式のサイズが指数的に増大してしまうので，Tseytin変換を用いる．Wikipediaの記事の通り変換すると，結構余計な変数を導入してしまう．以下のようにしたら良いように思う．まあ，後でSATソルバーが動くので，どれくらい益があるかわからないけれども．

基本的な考え方: 否定標準形の論理式 f を充足させたいとする．f の中に，a and b という部分があったとき，新しい変数 v を導入する．f が充足可能であることと， f’, not v or a, not v or b がみな充足可能であることが同値になる．ただし，f’ は， fk の a and b の部分を変数 v で置き換えたもの．

これを確認すると，まず，fが充足可能だとすると，その割当での a and b の値を v に割り当てれば，書き換え後の3つの論理式は充足される．逆に書き換え後の論理式が充足可能だとして，その割当で v が true であれば，a も b も true になるので，元の論理式列は充足される．vがfalseであるときには，fとf’は否定標準形なので，f は，a and b の部分が true であっても false であっても充足される．

ということで，論理式fが与えられたとき，以下の手続きで得られる節集合Cの全部が充足できることと，fが充足できることが同値になる:

f を否定標準形f0にする．「節集合」Cを空にして，「未処理論理式集合」Yをf0のみを含む集合として以下の手続きを繰返し行い，Yが空になったときのCが求めるものである．

• Yから一つ論理式gを取り出す．
• gがリテラル (変数やその否定) なら，gをCに追加する．
• gが and(h1, .., hn) なら，h1, …, hn を Y に追加する．
• gが or(h1, …, hn) の場合は，次のようにする．
  • h1, …, hn の中には or(…) の形のものが無いようにする．もし有ったら，リストに吸収してしまえば良い． (たとえば，or(v1, and(v2, or(v3, v4)), or(v5, or(v6, v7, v8), v9)) → or(v1, and(v2, or(v3, v4)), v5, v6, v7, v8, v9))
  • 各 j = 1, …, n に対して，リテラル xj と論理式の集合 Pj を次のように定める．
    • hj がリテラルなら，xj = hj．Pj は空集合．
    • hj が and(h1′, …, hm’) なら，新しい変数 v を導入して，xj = v．Pj = {or(not v, h1′), …, or(not v, hm’)}
  • そして，Cに，or(x1, …, xn) を追加し，各Pj の要素をすべて Y に追加する．