Tôi có thể tìm phương pháp nào để chuyển đổi một biểu thức boolean tùy ý thành dạng bình thường kết nghĩa hoặc không liên kết?

Question

Tôi đã viết a little app phân tích các biểu thức thành các cây cú pháp trừu tượng. Ngay bây giờ, tôi sử dụng một loạt các chẩn đoán đối với biểu thức để quyết định cách đánh giá tốt nhất truy vấn. Thật không may, có những ví dụ mà làm cho kế hoạch truy vấn vô cùng xấu.

Tôi đã tìm ra cách để có thể đoán rõ hơn cách truy vấn nên được đánh giá, nhưng tôi cần đặt biểu thức của mình vào CNF hoặc DNF trước để nhận được câu trả lời đúng. Tôi biết điều này có thể dẫn đến thời gian và không gian có khả năng, nhưng đối với các truy vấn thông thường người dùng của tôi chạy điều này không phải là vấn đề.

Bây giờ, chuyển đổi sang CNF hoặc DNF là thứ mà tôi luôn làm bằng tay để đơn giản hóa các biểu thức phức tạp. (Vâng, có lẽ không phải mọi lúc, nhưng tôi biết cách thực hiện bằng cách sử dụng pháp luật của demorgan, luật phân phối, v.v.) Tuy nhiên, tôi không chắc chắn cách bắt đầu dịch thành một phương pháp có thể triển khai như một thuật toán . Tôi đã xem xét các bài báo về tối ưu hóa truy vấn, và một số bắt đầu với "đầu tiên chúng tôi đưa mọi thứ vào CNF" hoặc "đầu tiên chúng tôi đưa mọi thứ vào DNF", và họ dường như không giải thích phương pháp của họ để hoàn thành điều đó.

Tôi nên bắt đầu từ đâu?

Answer 1

Thuật toán vani ngây thơ, cho công thức lượng hóa miễn phí, là:

• cho CNF, chuyển đổi sang negation normal form với luật De Morgan sau đó phân phối hay hơn và
• cho DNF, chuyển đổi sang negation normal form với De Morgan sau đó phân phối VÀ trên HOẶC

Không rõ ràng với tôi nếu công thức của bạn được định lượng. Nhưng ngay cả khi họ không, có vẻ như kết thúc của các bài viết wikipedia trên conjunctive normal form, và tương đương của nó - tương đương trong thế giới chuyên sâu tự động hóa - clausal normal form thay đổi cái tôi phác thảo một thuật toán có thể sử dụng (và trỏ đến tài liệu tham khảo nếu bạn muốn thực hiện chuyển đổi này thông minh hơn một chút). Nếu bạn cần nhiều hơn thế, vui lòng cho chúng tôi biết thêm về nơi bạn gặp khó khăn.

Answer 2

Nhìn vào https://github.com/bastikr/boolean.py Ví dụ:

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))) 

Output là:

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

CẬP NHẬT: Bây giờ tôi thích điều này 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

Tôi đã đi qua này trang: How to Convert a Formula to CNF. Nó cho thấy thuật toán chuyển đổi một biểu thức Boolean thành CNF trong mã giả. Giúp tôi bắt đầu vào chủ đề này.