問題タブ [conjunctive-normal-form]

基本的にデータソースとして機能する、インターフェイスする必要のあるライブラリがあります。データを取得するときに、特別な「フィルター式」をそのライブラリに渡すことができます。このライブラリは、後でSQLWHERE部分に変換されます。これらの表現はかなり制限されています。それらは連言標準形でなければなりません。好き：

もちろん、これはプログラミングにとってあまり快適ではありません。そこで、任意の式を解析してこの正規形に変換できる小さなラッパーを作成したいと思います。好き：

次のようなものに翻訳されます：

Ironyライブラリを使用して、式をツリーに解析できます。今、私はそれを正規化する必要があります、しかし私は方法がわかりません...ああ、また、ここにひねりがあります：

• 最終的な式には、NOT演算子を含めることはできません。ただし、演​​算子を逆演算子に置き換えることで、個々の項を逆にすることができます。だから、これはOKです：
  
  (not A or not B) AND (not C or not D)
  
  しかし、これはそうではありません：
  
  not (A or B) and not (C or D)
  
  
• 式は実質的に同一のSQLWHEREステートメントに変換されるため、式をできるだけ単純にしたいので、複雑なステートメントは実行速度を低下させる可能性があります。

次のような式がある場合：

(FA = すべての場合 / E = 存在する)

スコーレミゼーションのルールは次のように述べています。

1. E が FA の外にある場合、定数または
2. E が FA の内部にある場合、FA の外部からのすべての変数を引数として含む新しい関数に置き換えます。

では、この場合はどうすればよいでしょうか。Exists 量指定子を単に削除することはできますか、それとも定数に置き換えることはできますか?

ありがとう！

Espresso ロジック ミニマイザーを使用して、一連のブール方程式の最小化された形式を生成しています。ただし、プログラマブル アレイ ロジック (Espresso が通常使用されるもの) のロジックを生成するのではなく、これらを標準のマイクロプロセッサに実装することを検討しています。問題は、Espresso が結合正規形で出力を生成することです。これは PAL には最適ですが、x86 または PPC には最適ではありません。

たとえば、Espresso は XOR を完全に無視します。以下の Espresso 出力では、部分式(!B0&!B1&B2&!B3) | (!B0&!B1&!B2&B3)は と同等(!B0&!B1&(B2^B3))です。この置換により、式のゲート深度/クリティカル パスが増加しますが、周囲の任意の CPU の実行リソースを完全に飽和させるのに十分な数の項を含む式を見ていることを考えると、ゲート深度を減らすためにゲート深度をトレードオフすることが合理的であるように思われます。全体の命令数。また、関心のある一部のプロセッサで利用可能な ANDC や NOR などの命令の使用方法を理解するために、それを拡張したいと思います。

私が見ているCNF式の例：

したがって、これを実際の質問にするには; 優先順:

私が望む種類の表現を生成する Espresso のオプションまたは拡張機能を知っていますか?

PALのCNFを生成するだけでなく、さまざまなゲートタイプを理解する（または教えることができる）ブール論理最小化のためのツールを知っていますか？

上記のような CNF 式から、追加のタイプのゲートを使用した式に変換するアルゴリズムを知っていますか?

そのためのアルゴリズムを知らない場合、これを行う際に役立つヒューリスティックを知っていますか、または考えることができますか?

（そして、あなたがそれを提案しようとしていた場合に備えて-テストでは、GCCとICC（または、存在する他のCコンパイラー）は、CNF式からプロセッサー固有の最小化を行うほど賢くないことが示されています-それは本当に素晴らしいことですが、両方の -O3 -S の出力を調べると、XOR を使用できるケースをキャッチすることさえできないことがわかります)。

節を結合的な通常の形式に変換したいと思います。プログラムを実行するたびに句が変更されるので、これを行うにはプログラムにツールを組み込む必要があると思います。これを実装する方法について何か提案はありますか？
Orbitallibraryのようなライブラリも見つかりました。私は論理プログラミングに不慣れで、それらを使ったことがないので、それらを通り抜けるのは非常に困難です。私も物事を片付けるための例を見つけようとしましたが、何も思い浮かびませんでした。私は自分のプログラムをJava言語で構築しています。助けてください...

前もって感謝します！

3-cnf-sat 問題を次のように変更した場合:
各 c _iについて、 c _i = -x _i1 OR -x _i2 OR x _i3は、変数の 1 つだけが否定なしで表示されることを意味します。
また、x の一部 (またはすべて) に値 (0 または 1) が与えられます。
多項式時間で問題を解決できる必要があります (問題を満たす x の値を見つけるか、問題が満たされないことを証明します)。

1. この問題を解決する多項式実行時間アルゴリズムは何ですか?
2. 多項式時間で実行されることを証明します。

ヒント: c _i = -x _i1 OR -x _i2 OR x _{i3が c = (x i1} AND -x _i2 ) -> x _i3と等しいことを示す

ブール式の充足可能性をチェックするために sat ソルバーを使用する必要があります..

このような複雑なブール式があります

satソルバーに直接渡すことができる自動cnfファイルコンバーターはありますか?

cnf形式のファイルを読んだのですが、この式を.cnfファイルでどのように表現すればよいのでしょうか? 括弧内に接続詞があると混乱し、 --> と <-> をどのように表現するか? 私を助けてください

Prolog を学習しながら、CNF 問題 (パフォーマンスは問題ではありません) を解決するプログラムを作成しようとしたため、次のコードを解決することになりました(!x||y||!z)&&(x||!y||z)&&(x||y||z)&&(!x||!y||z)。

この宣言型言語を使用して CNF を解決する、より簡単で直接的な方法はありますか?

そのため、Visual Studio 2010でクエリを作成していました（つまり、サーバーエクスプローラーを開き、サーバーを右クリックして[新しいクエリ]を選択しました）。クエリには条件が含まれています

これは連言標準形（CNF）です。クエリ（MSSQL Server 2008に接続されている）を実行すると、テキストが次のように変更されました。

これは選言標準形（DNF）です。

私がオンラインで見つけた小さなことから、DNFはSQLが接続詞を別々に実行し、最後にそれらを結合することを可能にしているようです。

しかし、このようなものでは、非常に多くの条件が繰り返されるため、DNFは実際にCNFよりも優れていますか？そうでない場合、オプティマイザーに条件をそのまま取得させるにはどうすればよいですか？もしそうなら、それはより短くてきれいなので、アプリケーションコードでCNF形式でクエリを書くべきですか、それともオプティマイザーの時間を節約するためにDNF形式で書くべきですか？

MiniSatを使用して制約充足問題を解決しようとしています。一次論理では、問題はいくつかの離散ドメイン変数といくつかの述語によって簡単に表されます。

しかし、MiniSat は、これまで見てきた他の CSP ソルバーと同様に、すべて CNF 形式での入力を必要とします。そこで、一次論理式を CNF に変換する一種の「プリプロセッサ」を探しています。

何かご意見は？

ブール関数は、選言標準形（DNF）または連言標準形（CNF）で表すことができます。これらのフォームが役立つ理由を誰かが説明できますか？