問題タブ [sat]

3SAT の興味深いアルゴリズムを実装したいと考えていましたが、同じものをコーディングできなかったため、実際に機能するかどうかを確認できませんでした。このアルゴリズムは、次の Microsoft Word ファイルで定義されています: DropBox Link for 3SAT アルゴリズム このアルゴリズムが実際に機能するかどうか、また機能するかどうかはわかりません。しかし、その複雑さについて本当に知りたいです。これが多項式時間であるかのように、これに関して私を助けてください。そうすれば、P = NPが証明されます!

Mac でグルコース SAT ソルバーをコンパイルすると、グルコース 3.0 のコンパイル時に次のコンパイル時エラーが発生します。これらのエラーを回避するにはどうすればよいですか?

固定長ビット配列と比較して、16 ビットの符号付き整数変数を間隔 (-32768..32767) として表すと、パフォーマンスが大幅に低下するのはなぜですか?

前処理された NuSMV/NuXMV モデルを調べると、間隔タイプが列挙型に変換されていることがわかります。

ただし、BDD の統計には、関連する情報は表示されません。

たとえばミニサットのような SAT ソルバーについて話すとき、「0-depth」と「CNF 割り当て」の値は何を意味しますか? これらの値は通常、さまざまな SAT ソルバーの情報出力の一部です。

を使用して大きなCNF 式を解こうとしていSAT solverます。数式 ( DIMACS形式) には4,697,898,048 = 2^32 + 402,930,752句があり、私が見つけたすべての SAT ソルバーで問題が発生しています。

• (P)lingelingは、「節が多すぎる」(つまり、ヘッダー行が指定するよりも多くの節がありますが、そうではありません) があることを報告します。
• CryptoMiniSat4とpicosatは、2^32 が少なすぎる 402,930,752 句とヘッダー行を読み取ると主張しています。
• Glucoseは 98,916,961 節を解析し、単純化を使用して UNSAT として式を解いたと報告しているようですが、これが正しいとは考えられません (この短い式の最初のセグメントは SAT である可能性が非常に高いです)。

このサイズのファイルを処理できる SAT ソルバーを知っている人はいますか? または、この種の動作を回避できるコンパイラ スイッチのようなものはありますか? すべてのソルバーは64 ビット Linux用にコンパイルされていると思います。(これほど大きな数字を扱うのはちょっと初心者です、すみません。)

ACIS ファイル操作用のスクリプトを作成する必要があります。たとえば、次のようになります。

3D モデルを使用して CAD ソフトウェアからエクスポートされた 1 つの SAT ファイルがあり、SAT ファイルを開くスクリプトをいくつかの言語 (php、python など、動作する場合は .BAT でさえも) で作成し、内部のすべてのコンポーネントを削除したいと考えています。私の3Dモデル。3Dモデルの外側が欲しいだけです。

これを行う方法はありますか？SATファイルを見ると、大量のテキスト行があるため、おそらくRFCといくつかのトリッキーなツールを使用してこれを行うことができます..

何かアイデアはありますか？

よろしく、 ペドロ・ビエイラ

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

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

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

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

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

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