boolean-logic - ブール関数、DNFとCNFの目的は何ですか？

Question

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

Answer 1

CNF が便利なのは、この形式がブール SAT 問題を直接記述しているからです。この問題は NP 完全ですが、多くの不完全でヒューリスティックな指数時間ソルバーがあります。CNF は、ほとんどのソルバーが操作できる「 DIMACS CNF ファイル形式」と呼ばれるファイル形式にさらに標準化されています。したがって、たとえば、チップ業界は、DIMACS CNF に変換し、利用可能な任意のソルバーにフィードすることで、回路設計を検証できます。Tseitin Transformationは、回路を等充足可能なCNFに変換できます。

DNF は実際にはあまり役に立ちませんが、式を DNF に変換すると、式を満たす可能性のある代入のリストが表示されます。残念ながら、式を DNF に変換することは一般的に難しく、指数関数的な爆発 (非常に大きな DNF) につながる可能性があります。これは明らかです。

CNF は DNF と比較して簡潔にできますが、たとえば回路から変換すると構造が失われる可能性があるため、推論するのが難しい場合があり、別の簡潔な形式が役立ちます。and-inverter グラフのデータ構造は、この目的のために設計されました。回路の構造をより厳密にモデル化できるため、一部のタイプの式で推論するのがはるかに簡単になります。ただし、それを操作するソルバーは多くありません。

その他の形式は次のとおりです。

• 二分決定図
• 命題有向非巡回グラフ
• 否定の標準形
• その他（ウィキペディア）

Answer 2

関数を標準的な方法で表現すると役立ちます。これにより、多くのアルゴリズムを自動的に通過することが容易になります。

両方の形式は、たとえば、自動化された定理の解決、つまり解決方法の CNF で使用できます。