13

式を解析して抽象的な構文ツリーにする小さなアプリを作成しました。現在、クエリを最適に評価する方法を決定するために、式に対して一連のヒューリスティックを使用しています。残念ながら、クエリ プランを非常に悪くする例があります。

クエリがどのように評価されるべきかについて、証明可能なより良い推測を行う方法を見つけましたが、証明可能な正しい答えを得るためには、最初に式を CNF または DNF に入れる必要があります。これにより時間と空間が指数関数的になる可能性があることはわかっていますが、ユーザーが実行する通常のクエリではこれは問題ではありません。

さて、CNFやDNFへの変換は、複雑な式を簡略化するために、いつも手作業で行っています。（まあ、いつもではないかもしれませんが、デモガンの法則、分配法則などを使用してそれがどのように行われるかは知っています。）しかし、それをアルゴリズムとして実装可能なメソッドに変換する方法がわかりません。私はクエリの最適化に関する論文を見てきましたが、いくつかは「最初に CNF に入れます」または「最初に DNF に入れます」で始まり、それを達成するための方法を説明していないようです。

どこから始めればよいですか？

4

3 に答える 3

9

量指定子のない数式の単純なバニラ アルゴリズムは次のとおりです。

  • CNF の場合、ド・モルガンの法則を使用して否定正規形に変換し、AND の上に OR を分配します。
  • DNF の場合、ド モルガンの法則を使用して否定の正規形に変換し、OR の上に AND を分配します。

あなたの式が定量化されているかどうかは私にはわかりません。しかし、そうでなくても、接続法正規形に関するウィキペディアの記事は終わりのようであり、自動化された定理証明者の世界ではほぼ同等です -クローザル正規形の分身は、使用可能なアルゴリズムの概要を説明しています (必要に応じて参考文献を参照してください)。この変換をもう少し賢くするため)。それ以上必要な場合は、どこで問題が発生したかをお知らせください。

于 2011-11-03T11:41:37.857 に答える
4

私はこのページに出くわしました: How to Convert a Formula to CNF . ブール式を疑似コードで CNF に変換するアルゴリズムを示します。このトピックを始めるのに役立ちました。

于 2016-10-18T09:41:40.847 に答える