9

SMT-Solver は、制約の解決に使用できます。私たちが知っているように、CSP ソルバーは長年にわたって制約解決にも使用されてきました。では、CSP ソルバーに対する SMT ソルバーの利点は何でしょうか?

4

1 に答える 1

4

それは完全にあなたが何をしたいかによって異なります。両方を SAT に変換し、制約の問題を SAT 問題として解決できます。制約ソルバーは通常、問題のモデル化に関して最高レベルの抽象化を提供します。SAT ソルバーは非常に高速ですが、問題によっては SMT または制約ソルバーの方が高速な場合があります。

あなたの質問に対する一般的な答えはありません。それはあなたの特定のユースケースに依存します。

于 2012-05-14T16:37:09.727 に答える