5

SATがNP完全であるという証明は構成的証明であるため、プログラムとして実装できるはずです。誰かがこれをしましたか？

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

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

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式には他の補助変数があるため、コンパイラーはどの変数が証明書に対応するかを示す必要があります。

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

4

1 に答える 1

3

SMT ソルバーは、必要なものに最も近いものであるため、調べる必要があります。SMT (ループなし) を使用して完全なチューリング言語で記述しているわけではありませんが、整数変数と実数値変数、ブール論理、関数、基本的な算術演算、および配列を操作できます。

于 2012-01-26T19:57:27.070 に答える