問題タブ [conjunctive-normal-form]

正の命題式を選言標準形 (DNF)に圧縮したいと思います。

今のところ、否定されたリテラルのない単純な DNF のみを想定しています。逆のプロセス、解凍は簡単に定義できます。論理積と論理和のみから構築された数式の場合、次の書き換え規則によって DNF が生成されます。

解凍の例を次に示します。

ここで、DNF から単一の数式を生成できるアルゴリズムがいくつかあるのではないかと考えています。私はすでに二分決定図を調べました。私がこれらの問題を抱えているのは、途中ですべての選言を組み合わせることができないということです。

たとえば、共有を使用する二分決定図のアルゴリズムは、印刷中に同様の分岐を表示したり、新しい前置詞変数を導入したりしますが、どちらも望ましくありません。

結果は、もはや DNF ではなく、単一の式になるはずです。これは、元の DNF に既にある前置詞変数と、選言と接続詞のみを使用する二分決定図アルゴリズムよりもコンパクトです。必要な圧縮の例を次に示します。

あなたはどう思いますか？Prolog の実装が優先されます。

さよなら

評価したい論理式があります。式は入れ子にすることができ、T (True) または F (False) と括弧で構成されます。括弧 "(" は「論理 OR」を意味します。2 つの用語 TF が隣り合っている場合 (または他の 2 つの組み合わせが隣り合っている場合) は、ANDED (論理 AND) である必要があります。

たとえば、式:

この問題を解決するためのアルゴリズムが必要です。最初に式を論理和または論理積の正規形に変換してから、式を簡単に評価できるようにすることを考えました。しかし、式を正規化するアルゴリズムが見つかりませんでした。助言がありますか？ありがとうございました。

問題の説明はここにあります: https://icpcarchive.ecs.baylor.edu/index.php?option=com_onlinejudge&Itemid=2&category=378&page=show_problem&problem=2967

編集：問題の一部を誤解しました。与えられた論理式では、AND/OR 演算子はすべての括弧 "(" と交互に使用されます。式をツリーで表す場合、AND/OR 演算子はサブツリーの深さレベルに依存します。ただし、最初に、最も深いレベルのツリーは AND ツリーであると仮定しました. 私の仕事は、おそらくツリーを構築することによって、与えられた式を評価することです. 問題の正しい要件を明確にした以下の回答に感謝します.

here で説明されている標準に従って、cnfを保存するファイルからcnfをロードするコードをいくつか作成しました。

ファイルは次のとおりです。

[[1, -3][2,3,-1]] にロードしたい

私が書いたコードは機能しますが、私には醜いようです。それについて何らかのフィードバックをいただければ幸いです。（私はpythonが初めてです）。

ありがとう ！

1 つの例、2 つの質問、2 つのアイデア:

1) 自然言語でそれはどういう意味ですか?

at(opic) があり、as(tudent) が a(人工知能) で t(opic) を学習し、気が散らない場合、この s(tudent) は a(i) で試験に合格します。

2) その CNF は?

どう思いますか？

Z3 を使用して、それぞれ 22 個の入力を持つ数百の XOR 句を含む充足可能性の問題を解決しています。XOR 句を DIMACS 形式でコーディングするために、Tseitin エンコーディングを使用しています。私の変換では、XOR をそれぞれ最大 5 つのリテラルを持つ小さな CNF 句に分割します。これまでのところ、Z3 は SAT ソリューションを考案できていません。

エンコーディングを改善するにはどうすればよいですか?

ガウスの消去法を見てきましたが、XOR 式には同じ入力変数がないため、これはおそらく役に立ちません。

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

この方法で構築された整形式の論理積があるかどうかを判断する関数を構築する必要があります。

cong ::= '(' と wff wff ...')'

数式が wff かどうかを判断するコードがあるとします。この関数は、リストの最初の要素が wff であるかどうかを最初にチェック'and し、残りのサブリストが wff であるかどうかを再帰的にチェックする必要があります。これ pも wff であるため、必ずしもサブリストである必要はありません。

例 ：(and (or a b v) (and a b d) m n)

これが私が試したもので、うまくいきません：

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

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

私が持っているブール演算子と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 を見てください」または「ええ、あなたの考えは正しいです。楽しんでください!」のようなものであっても、フィードバックをいただければ幸いです。

Java で CNF 演算子を実行しようとしていますが、等式でエラーが発生します。

まず、ほとんどのソフトウェアを作成しましたが、完全には作成しませんでした。

私のコードはここにあります：

問題は平等です。

プログラムは、変数がtrueまたはであることを確認する必要がありますfalse。

例えば ​​：

このプログラムは次のようになります。

p : 1 の数を与える (ユーザーは数字の 1 ( true) またはゼロ ( false)
を与える) q の数を
与える : 0 s の数を与える : 1
t の数を
与える : 0 k の数を与える : 0
(変数が複数使用する場合、プログラムは 1 回尋ねます)

これらの変数を見ると、(1 または 0 または 1 または 0 または 0) と (1 または 0) が true を返すことがわかりますが、これはできません。やり方がわかりません。

幸運をお祈りしています。