任意のブール式を結合型または論理和型に変換する方法は、どこで見つけることができますか？

Question

私は式を抽象構文木に構文解析するa little appと書いています。今、クエリに対して最も良い評価をする方法を決定するために、式に対して一連の発見的手法を使用します。残念ながら、クエリプランを極端に悪化させる例があります。

質問の評価方法を推測する方法がわかりましたが、確かに正解を得るためには、まず式をCNFまたはDNFに入力する必要があります。私はこれが潜在的に指数関数的な時間と空間をもたらす可能性があることを知っていますが、典型的なクエリではユーザーはこれを実行しても問題ありません。

ここで、CNFまたはDNFに変換することは、複雑な表現を簡素化するために常に手作業で行うことです。 （まあ、はいつもですが、私はそれがdemorganの法則や分布法などを使ってどうやっているのか分かります）しかし、それをアルゴリズムとして実装可能な方法に変換する方法はわかりません。私はクエリの最適化に関する論文を見てきましたが、「まず最初に私たちは物事をCNFに入れます」または「最初に物事をDNFに入れる」というものから始まり、それを達成する方法を決して説明していないようです。

どこから始めたらよいですか？数量詞フリー式のため

Answer 1

ナイーブバニラアルゴリズムは、次のとおりです。CNFのため

• 、ド・モルガンの法則とnegation normal formに変換後、配布、または超えると
• DNFのために、ド・モルガンとnegation normal formに変換法律はそれからAND以上を配付します

あなたの数式が定量化されるかどうかは私には不明です。しかし、たとえそうでないとしても、conjunctive normal formに関するウィキペディアの記事の終わりと思われます。自動化されたテルモの証明者の世界では、おおよそ同等です。clausal normal form少し賢い）。それ以上のものが必要な場合は、難点に遭遇した場所について詳しく教えてください。

Answer 2

https://github.com/bastikr/boolean.py 例を見て：

def test(self): 
    expr = parse("a*(b+~c*d)") 
    print(expr) 

    dnf_expr = normalize(boolean.OR, expr) 
    print(list(map(str, dnf_expr))) 

    cnf_expr = normalize(boolean.AND, expr) 
    print(list(map(str, cnf_expr))) 

出力は次のとおりです。

a*(b+(~c*d)) 
['a*b', 'a*~c*d'] 
['a', 'b+~c', 'b+d'] 

UPDATE：今、私はこのsympy logic package好む：

>>> from sympy.logic.boolalg import to_dnf 
>>> from sympy.abc import A, B, C 
>>> to_dnf(B & (A | C)) 
Or(And(A, B), And(B, C)) 
>>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True) 
Or(A, C) 

Answer 3

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