Existential Quantification as Incremental SAT https://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkk11a.pdf : 命題論理式の量化子除去をやるのにBDDとか使うのではなくSATソルバでという話。
dual-rail encoding で解列挙すればimplicantが列挙できるので、基数制約(cardinality constraint)を使って小さい方から列挙することで、shortest implicant を列挙。これらのimplicantの選言としてDNF φ が得られるので、今度はCNF ¬φ に対して同じことをすると、 ¬φ の implicant J が得られるが、待遇を取ると¬Jはφのimplicateとなっている。 こうしてimplicateを集めることで元の論理式から存在量化された変数を消去したCNFを得ることができる。
非常に単純で良いのだけど、少なくとも上記のPDFは、τ(ω)の定義でプラス・マイナスが逆になっている気がするのと、あと2.3で得られたcubeから削れるリテラルを削ろうとしているのが良くわからなかった。 基数制約を使って小さい方から列挙しているのだから、削った結果が先に列挙され、ブロッキング節が追加されるので、そういう場合は起こり得ないのでは？