ヒビルテ(2012-08-26)λ. Tseitin encoding と pseudo boolean constraint 任意の命題論理式は Tseitin encoding というを使うと、元の論理式に対して線形サイズであるような equisatisfiable なCNFへと変形できる。 SATソルバを使うためにCNFを作る - soutaroにっき 自分で昔書いたやつ その際に、連言 l1∧…∧ln を表現するために、新たな変数cと ￢l1∨…∨￢ln∨c (すなわち l1∧…∧ln → c) および ￢c∨li (すなわち c→li) という形の節を導入し、もとの連言をcで置き換える。ただし、PB制約(Pseudo Boolean constraint)が使える場合には、後者の ￢c∨li という形のn個の節の代わりに n*c ≦ l1+…+ln という形の単一のPB制約を加えても良いことが知られている。 し
