問題タブ [satisfiability]

誰かが O(n^3) 時間で CNF ブール式を与えられたグラフを作成する方法を見つけ、この特別なグラフのスパニング ツリーが CNF 方程式の解になるとします。

このシナリオは、誰かが SAT 問題の解決策を見つけ、O(n^3) 時間で実行されるガジェット (リダクション) を使用して SAT 問題をスパニング ツリー問題に還元することで P=NP を解決したことを暗示しているようです。

しかし、彼らのアルゴリズムが作成するグラフに n があるとしたらどうでしょう! または2 ^ nノードとエッジ？

そのシナリオでは、DFS や BFS などのスパニング ツリー アルゴリズムがノード/エッジの数に対して線形時間で実行される可能性がありますが、ブール式への入力の数に対してポリゴン時間で実行されることはありません。そのため、完全な解を実行するには n! 評価する時間。

この推論は正しいですか？

私は頭の中にプロジェクトがあり、似たようなことが以前に行われたかどうかに興味があります。さまざまなタイプの制約のセットがあり、これらの制約を一緒に満たすことはできないとします。

C = {c1、c2、c3、...、cn}

(c1 and c2 and c3 ... cn) : 満足できない

私の目的は、このセットを k 個のセット (おそらく k は非常に小さい) に分割して、すべての制約セットが個別に満たされるようにすることです。

基本的な解決策は、貪欲なアプローチを使用することです。制約は最初の制約として選択され、最初のグループとしてラベル付けされます。次に、2 番目の制約が選択され、最初の制約で解けるかどうかがチェックされます。それらが解決可能である場合、2 番目の制約も最初のグループに含まれます。それ以外の場合は、2 番目のグループとしてラベル付けされます。このプロセスは、セットに制約がなくなるまでこの方法で続行されます。これを行う別の方法は、制約を 2 つのセットに分割し、これらのセットが個別に解決可能かどうかを確認することです。そうでない場合は、再帰的に分割を続けます。これら 2 つのアプローチはどちらもサイズが大きくなり、制約セットを非常に小さなセットに分割します。

k が最適値 (最小の k 値) に近い k セットに制約セットを分割する効率的な方法を探しています。ここには 2 つの課題があります。1) スケーラビリティの問題と 2) 制約の構造が事前にわかっていないことです。

私は sat4j ソルバーがまったく初めてで、ブール値の満足可能な問題を研究しています。そして私は立ち往生しています。ブール式の整数変数を解くプログラムを作りたいです。

x1 < x2 + x3 ユーザーがその数式を入力すると、私のプログラムは x1 = 5 、 x2 = 3 、 x3 = 4 のようにこの数式を満たします (true を返します)。したがって、数式は true を返し、ユーザーは数式を満たすこの整数値を取得します。私はJavaでEclipseで作業しているため、sat4jで作成することは可能です。

これは、始めるための宿題の質問です。始める前にいくつか質問があります。

私たちの問題は次のとおりです。

「次のように k-Independent Set から 2-SAT に還元します。n 個の頂点を持つグラフ G が n 個の命題から成り、頂点ごとに 1 つです。頂点 i が独立したセットに属している場合、頂点 i の各命題 xi は true に設定されます。すべてのエッジ (u,v) について、u と v の両方が独立集合に属することはできないという節を書きます。」

私の質問は、私が読んだものはすべて、2-SAT は NP 完全問題ではないということです。では、独立集合の問題からどのように削減できるのでしょうか?

Z3 で仮定を表現する方法はありますか (私は Z3Py ライブラリを使用しています)、エンジンがそれらの有効性をチェックせず、定理の証明のように、それらを基礎となる理論として採用するようにしますか?

たとえば、Real 型の引数を持つ 2 つの単項関数があるとします。すべての入力値について、f1(t) が f2(t) と等しいことを Z3 エンジンに伝えたいと思います。

次のような Z3Py でエンコードされます:
t = Real("t"
)

提示されたコードの問題は、アサーション セットが非常に大きく、量指定子を使用していることです (リアルタイム システムの充足可能性を証明しようとしています)。上記のアサーションを他のアサーションのセットに追加すると、チェック手順が終了しません。

タイトルがすべてを物語っています。-1 を次のように提示しようとします: (_ bv-1 32)、および z3 は文句を言います。

3x - 5y <= 10ビットベクトルなどの制約を提示するにはどうすればよいですか? 何らかの理由で、線形整数を使用したくありません。