問題タブ [satisfiability]

Javaで実装されたGSATおよびSA-SATアルゴリズムを探しています。誰かがそれについて知っていますか？ありがとうございました。

SMT-Solver は、制約の解決に使用できます。私たちが知っているように、CSP ソルバーは長年にわたって制約解決にも使用されてきました。では、CSP ソルバーに対する SMT ソルバーの利点は何でしょうか?

SMT ソルバーは、SAT と同様に充足可能性を考慮して開発されています。私たちが知っているように、SATは充足可能性のためでもあり、SATの変形が提案されています。それらの 1 つが max-SAT です。そこで、max-SMT ソルバーが存在するかどうか、存在する場合はどのように機能するのかをお尋ねしたいと思います。

私はブール式を持っています: (x_{1} or x_{2}) and (x_{3} or x_{4}) and ..... and (x_{2r-1} or x_{2r}) , x_{i}はセットに属します: {p_{1}, p_{2}, ... p_{99} , ~p_{1}, ~p_{2}, ... ~p_{99} } x_{i}のいくつかの値について、与えられた式が真であるかどうかを判断する必要があります。

私はそれが一般的に計算的に難しいことを知っています。しかし、この特定の問題を解決できる非常に高速な方法はありますか? これまでのところ、私はバックトラックを試みました - つまり、再帰では、すべての可能な変数に対してすべての可能な値 (0 または 1 のように多くはない) を代入し、まだ値を取得していないすべての変数は自明に真です。再帰を深く掘り下げる前に、(すべての変数が値を持っているわけではない場合でも) 式をチェックし、それが偽の場合は深くは考えません。しかし、遅すぎます。何か案は？大変助かりました。

非常に興味深い質問だと思ったものへの回答を書きましたが、残念ながら、投稿する前にその質問は作成者によって削除されました。他の人に役立つ可能性がある場合に備えて、質問の要約と回答をここに再投稿します。

結合正規形のブール式が与えられると、解 (式を満たす変数割り当て) または問題が満たされないという情報を返す SAT ソルバーがあるとします。

このソルバーを使用してすべての解を見つけることはできますか?

式のセットが与えられた場合、 内のすべての式を意味する最小のサブセットをs見つけたいと思います。のすべてのペアについて、 は意味を持たず、その逆も成り立つため、私は最小の独立集合と呼びます 。s'sssa,bs'ab

O(2^|s|)単純なアプローチは複雑になるように思えます。より効率的な方法はありますか？この問題は、現在の smt/sat ソルバー (unsat コアなど) を利用できる方法でエンコードできますか?

いくつかの変数が特別にマークされている CNF 式があるとします。
SAT ソルバー (minisat など) に真に割り当てられた特殊変数の数を最大化するソリューションを見つける方法はありますか?

m * nのバイナリ行列A、m * pのバイナリ行列Bが与えられます。ここで、n> m AX=BとなるようにXを計算するための効率的なアルゴリズムは何ですか。

例えば：

私がバイナリ行列と言うとき、私は体Z_2で定義された行列を意味することに注意してください。つまり、すべての算術はmod2です。

興味がある場合、これはランダムエラー訂正コードに適した行列を生成する際に私が直面している問題です。

これが私の問題です。SA​​T問題（満足可能性）でMatlabに行き詰まりました

実際にはDPLLと呼ばれる関数が必要です。ここのどこかで見ましたが、Javaで書かれています。誰か助けてもらえますか?

私は、未知の値がたくさんある問題を解決する実用的な方法 (たとえば、エンジニアリングの努力の観点から) を探しています。

最終的にブール値を返す (メモリ内の) バイナリ ツリー式。

私が持っているブール演算子とand or xor not32 ビット整数には、比較、加算、乗算、除算 (注: これらは 32 ビット オーバーフローを尊重する必要があります!) のようなものと、いくつかのビット単位のもの (シフト、ビット単位の &、|) があります。 ^ )。しかし、必ずしもすべての操作をサポートする必要はありません [参照: LOL_NO_IDEA ]

そして、次の 3 つの答えのいずれかを取得したいと考えています。

• ES_POSSIBLE [方法を知る必要はありません。その方法が存在することを伝えてください]
• 不可能[私の変数がどんな値を保持していても、この等式は決して真ではありません]
• LOL_NO_IDEA [問題が複雑すぎるか時間がかかる場合、これは許容されます]

私が解決している問題はどれも、過度に大規模または複雑で、用語が多すぎるものではありません (ほとんどの場合、数百のオーダーです)。そして大量の LOL_NO_IDEA を持っていても問題ありません。ただし、私はこれらの問題を何百万も解決しているため、一定のコストがかかります (たとえば、テキスト形式に変換し、外部ソルバーを呼び出します)。

私はこれを scala から実行しているので、SAT4J を使用することは非常に魅力的です。ただし、ドキュメントはひどいものです（特に、このSATの世界を数日間しか調べていない私のような人は）

しかし、私の現在の考えは、最初にすべての Int32 を 32 のブール値に変換することです。そうすれば、入れ子になったブール式として (a < b) のような関係を表現できます (msb を比較し、それらが eq の場合は、次に、など)。

そして、ブール変数とブール式の大きな式ツリーがある場合、それをトラバースして、次のように段階的に構築します: http://en.wikipedia.org/wiki/Conjunctive_normal_form

それをSAT4Jに供給します。

ただし、これはすべて非常に困難に見えます。CNF を構築することでさえ、非常に非効率的であり (私が実装したような単純な方法で行う)、エラーが発生しやすいようです。すべての整数演算をブール式としてエンコードしようとすることは言うまでもありません。また、SAT 解法を主にブラック ボックスとして使用したいという問題を抱えたエンジニアである、私のような人向けに設計された優れたリソースを見つけることができませんでした。

「笑、あなたのばか - X を見てください」または「ええ、あなたの考えは正しいです。楽しんでください!」のようなものであっても、フィードバックをいただければ幸いです。