問題タブ [sat-solvers]

C# 実装で Z3 sat ソルバーを使用しようとしています。このコードは、Microsoft 自身が " http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs "で示した例に非常に近いものです。私のコードは次のとおりです。

しかし、このモデルの「s.UnsatCore」に到達しても、空です。

また、次のようなアサーションを入力しようとしました。

UnsatCore が "constraint1, constrint3" を返すようにしたいと思います。私が間違っていることについて誰かが私を助けることができますか?

SAT ソルバーに必要な形式に操作する必要がある DIMACS cnf 形式のファイルがあります。

具体的には、次のものを取得する必要があります。

に

助けてくれてありがとう！

ホーン式が充足可能かどうかを証明する方が簡単であることはわかっています。私の質問は: 通常の CNF よりもホーン式の方が簡単なのはなぜですか?

今、私はSAT解法について書いていますが、ある時点で立ち往生しています。あなたが私を助けてくれることを願っています。

SAT-Problems を解決するいくつかの方法について説明したいと思います。現在、次の 3 つの方法があります。

1. 強引な
2. ランダム (ナイーブ)
3. DPLL (ヒューリスティックが異なる)
4. ? ない ？
5. ...

私の問題は、唯一の効果的なアルゴリズムが DPLL (および DPLL とはわずかに異なる他のアルゴリズム) であることです。したがって、DPLL と比較するものは何もありません。

私の質問: 比較できる DPLL (DP) に基づいていないアルゴリズムをいくつか教えていただければ幸いです。

以下は私が見つけたもののいくつかです。

• モニエン・スペッケンマイヤー
• ダンツィン、ゲルト、ヒルシュ、シェーニング
• Paturi-Pudlák-Zane-アルゴリズム
• ホフマイスター、シェーニング、シューラー、渡辺

ご協力いただきありがとうございます。

たとえばミニサットのような 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用にコンパイルされていると思います。(これほど大きな数字を扱うのはちょっと初心者です、すみません。)

私はSATの問題を解決しなければなりません。その問題には 2 つのカーディナリティ制約があります。最初の 1 つは、1 日あたり最大 6 つの「同じステージのクラス」、「大学」は 1 日 12 時間「開いている」ため、制約を生成して SAT ソルバーに適用する必要があります。

2 番目のカーディナリティ制約は次のとおりです。すべての被験者は、週に少なくとも X 時間必要です。

私は読んでいて、最初の最良の方法は「ネットワークアルゴリズムのソート」かもしれません.2番目についてはわかりませんが、実装方法もプロローグでの実装も開始していません。