SATソルバーで二次方程式を解く

元画像を表示

この記事はSYSKEN Advent Calendar 2021 19日目の記事です。

2週目が回ってきました、あらたです。

今回は夏休みの間に作っていたSATソルバーについて少し話をします。とはいえ、論理学を専攻しているわけではないので念のため以下にわかりやすい資料のリンクを貼っておきます。

https://jssst-ppl.org/workshop/2017/slides/ppl2017_c4_soh.pdf
https://rkx1209.hatenablog.com/entry/2017/12/17/175439

1. SATソルバーとは

次のような論理式を考えます。

(x1 | x2) & (!x1 | !x2)

x1とx2にfalseもしくはtrueを代入して、この論理式全体の値をtrueにできるでしょうか。答えは、可能です。例えばx1=true、x2=falseとしたときに、論理式全体の値をtrueにすることができます。このように、論理式が与えられたときに変数の値を適切に選んで、論理式全体の値をtrueにできるか判定する問題を、充足可能性問題（SAT問題: SATisfiability problem）と呼びます。そしてこの問題を解いてくれるようなプログラムをSATソルバーと呼びます。

今回は、このSATソルバーを使って二次方程式の解を求めることを目指します。

2. 1bit整数の演算

しかし、論理式を扱うSATソルバーに整数の問題が扱えるとは思えません。いったいどのようにして二次方程式を解かせればよいのでしょうか。

そのために、まずは計算機の仕組みに目を向けてみましょう。我々が使っているコンピューターは半加算器という組み合わせ回路を使って1bitの加算を実現しています。そしてこの回路では、0と1の二値を使って数を表現しています。共通点が見えてきました。

論理式においても、変数に代入できるのはfalseとtrueの二値のみです。つまりは、コンピューターと同じように行えば、論理式でも整数の演算を定義できるのではないのでしょうか。

はい、実は任意の組み合わせ回路はSAT問題に落とし込むことが可能であると知られています。そのために使うのが、Tseytin transformationです。例として、ANDゲートを取り上げてみましょう。Tseytin transformationにより、ANDゲートは次の論理式で表すことが可能です。

(!A | !B | C) & (A | !C) & (B | !C)

この論理式を充足するような変数A、B、Cの組は、常にC = A & Bの関係を満たしています。同様に、ORゲートやNOTゲート、XORゲートなども論理式で表現することが可能です。つまりは、論理式の世界で半加算器を実装してやれば、1bit整数の演算を定義できるというわけです。