21

従来、計算ロジックでのほとんどの作業は、SAT（充足可能性）ソルバーを使用する命題論理、または1次定理証明器を使用する1次のいずれかでした。

近年、基本的に命題論理を算術などの理論で補強するSMT（満足度モジュロ理論）ソルバーで多くの進歩が見られました。SRIInternationalのJohnRushbyは、彼らを破壊的技術と呼んでいます。

一階述語論理で処理できるが、SMTでは処理できない問題の最も重要な実際的な例は何ですか？特に、ソフトウェア検証の領域でSMTが処理できない問題はどのようなものでしょうか。

4

1 に答える 1

24

SMTソルバーは、SATソルバーほど強力ではありません。それらはまだ指数関数的な時間で実行されるか、SATの同じ問題に対して不完全です。SMTの利点は、SMTで明らかな多くのことが、同等のsatソルバーが再検出するのに長い時間がかかる可能性があることです。

したがって、ソフトウェア検証を例にとると、QF BV（ビットベクトルの数量詞なしの理論）SMTソルバーを使用すると、SMTソルバーは代わりに単語レベルで（a + b = b + a）を認識します。 SATソルバーが個々のブール値を使用していることを証明するには、非常に長い時間がかかる場合があります。

したがって、ソフトウェア検証では、SMTまたはSATソルバーでは難しいソフトウェア検証の問題を簡単に発生させることができます。

まず、ループはQF BVで展開する必要があります。つまり、実際には、ソルバーがチェックする対象を制限する必要があります。数量詞が許可された場合、NP完全だけでなく、PSPACE完全問題になります。

第二に、一般的に難しいと考えられている問題は、QFBVで簡単にエンコードできます。たとえば、次のようにプログラムを作成できます。

void run(int64_t a,int64_t b)
{
  a * b == <some large semiprime>;

  assert (false);
}

もちろん、SMTソルバーはassert（false）が発生することを簡単に証明しますが、入力を提供する反例を提供する必要がありますa,b。RSA半素数に設定 <some large number>すると、乗算が逆になります...整数因数分解とも呼ばれます。したがって、これはどのSMTソルバーにとっても難しい可能性があり、ソフトウェア検証が一般に難しい問題であることを示しています（P = NP、または少なくとも整数因数分解が容易にならない限り）。このようなSMTソルバーは、書きやすく、推論しやすい言語で物事をドレスアップすることにより、SATソルバーの足がかりになります。

より高度な理論を解くSMTソルバーは、より難しい問題を解こうとしているため、必然的に不完全であるか、SATソルバーよりも低速です。

参照：

  • 興味深いことに、ビーバーSMTソルバーはQF BVをCNFに変換し、SATソルバーをバックエンドとして使用できます。
  • LLVM IR（中間表現）にコンパイルされたプログラムを取得し、バグをチェックし、アサーションなどの反例を見つけることができるKlee。バグが見つかった場合は、正しさの反例を与えることができます（入力が得られます）バグを再現します）。
于 2012-09-16T01:56:03.733 に答える