3

ブール充足性問題は、ブール式の充足可能性をチェックするための一般化です。ここで、ブール式は多項式の非負アルゴリズムによって生成されます。多項式は、たとえば、変数の量がどこにあるか$x_1x_2+x_2x_3$など$x_1$、いくつかの間隔である可能性があります。現在、非負性などの多項式の機能を分枝限定アルゴリズムなどの特別なアルゴリズムを使用してチェックしています。このアルゴリズムでは、大きな問題を小さな問題にしますが、MiniSatなどの一部の SAT ソルバーで約束されている学習などの機能が欠けています。そう$x_i\in[0.1,0.3]\;\;\forall i=1,...,n$$n$

  1. 多項式関数や一般的な多変量関数などの多項式のプロパティをチェックするように設計された SAT ソルバーはありますか?

  2. 多変量関数と非負アルゴリズムをブール式に変換する簡単な方法はありますか?

4

1 に答える 1