検証アルゴリズムをSAT問題に変換するコンパイラ

Question

SATがNP完全であるという証明は建設的な証明であるため、プログラムとして実装することが可能である必要があります。誰もこれをしましたか？

私は入力としてプログラム（真または偽を返す）を取り、SAT式を出力するプログラム（コンパイラ）を探しています。

たとえば、コンパイラは入力として次のプログラム（pythonic構文で表示しますが、言語は問題ありません）を入力してSAT式を出力できます。 SAT式をSATソルバに供給すると、パラメータ「証明書」の解が得られます。この場合、解は{-3、-2、5}が解であることを示す[False、True、True、True、False]になります。

def verify(certificate): 
    problem = [-7, -3, -2, 5, 8] 
    sum = 0 
    for (x, b) in zip(problem, certificate): 
    if b: 
     sum += x 
    return sum == 0 

明らかに、出力SAT式には他の補助変数があるため、コンパイラはどの変数が証明書に対応しているかを示す必要があります。

このようなコンパイラは既に存在しますか？いずれもオープンソースですか？

Answer 1

あなたが望むものに最も近いので、SMTソルバーを調べる必要があります。あなたはSMT（ループなし）でチューリング完全言語を書いているわけではありませんが、整数値と実数変数、ブール論理、関数、基本的な算術と配列を扱うことができます。