問題タブ [satisfiability]

の ( )SMTLIB1.2に相当するものがあるのだろうか。と を使用してさまざまなエンコード テストを実行しています。問題は出力にあり、モデルが数百の補助変数値と混合されたすべての値を取得し続けます。SMTLIB2get-valueSMTZ3 SMT solverSMTLIB1.2

ありがとう

SAT ソルバーは、命題式 F の充足可能性を証明します。しかし、LTL 式の充足可能性をテストするために SAT を使用することは可能ですか? たとえば、次の LTL 式が満たされないことを証明できますか?

G (A => B) および (A = 真) および (B = 偽)

これを処理できる SAT ソルバーを教えていただければ幸いです。

どうもありがとうございました！

私は自分のアルゴリズム コースのために、Garey と Johnson による「 Computers and Intractability - A Guide to the Theory of NP-Completeness」という本を読みました。しかし、1 年後に資料を見直したときに、私はクックの定理を本当に理解していなかったことに気付きました。

証明に関しては、SAT が最初に NP であることが最初に示されている理由 (NP 完全の最初の要件) を理解していますが、「遺伝的」多項式の下で「他の」NP 完全問題を示す技術に苦労しています。 SATに変身。

誰かがこれをもっと骨抜きにした方法で説明できるかどうか疑問に思っていました.

このリンクで説明されている方法を使用して、すべてのソリューションを見つける方法を見つけました。

これは正常に動作していますが、遅いです。最初から制約を再計算するため、i_e は以前の計算を利用しません。

さて、この リンクで、MiniSat をライブラリとして使用してすべての解を見つけるより効率的な方法があることを確認しました。しかし、その方法はそこには記載されていません。

すべての SAT ソリューションを効率的に見つけるための適切なドキュメントを教えてください。

ありがとう。

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