¿Dónde podría encontrar un método para convertir una expresión booleana arbitraria en una forma normal conjuntiva o disyuntiva?

Question

He escrito a little app que analiza expresiones en árboles sintácticos abstractos. En este momento, uso un montón de heurísticas contra la expresión para decidir cómo evaluar mejor la consulta. Desafortunadamente, hay ejemplos que hacen que el plan de consulta sea extremadamente malo.

He encontrado una manera de mejorar las conjeturas sobre cómo se deben evaluar las consultas, pero primero debo poner mi expresión en CNF o DNF para obtener respuestas correctas. Sé que esto podría resultar en tiempo y espacio potencialmente exponenciales, pero para las consultas típicas mis usuarios ejecutan esto no es un problema.

Ahora, la conversión a CNF o DNF es algo que hago a mano todo el tiempo para simplificar expresiones complicadas. (Bueno, tal vez no todo el tiempo, pero sé cómo se hace usando, por ejemplo, leyes de demorgan, leyes distributivas, etc.) Sin embargo, no estoy seguro de cómo comenzar a traducir eso en un método que se puede implementar como un algoritmo . He visto documentos sobre optimización de consultas, y varios comienzan con "bueno, primero ponemos cosas en CNF" o "primero ponemos cosas en DNF", y nunca parecen explicar su método para lograr eso.

¿Dónde debería empezar?

Answer 1

El algoritmo de vainilla ingenuo, de fórmulas libres de cuantificador, es:

• para CNF, convertir a negation normal form con las leyes de De Morgan entonces distribuyen o más y
• para DNF, convertir a negation normal form con De Morgan las leyes luego distribuyen AND sobre O

No está claro si sus fórmulas están cuantificadas. Pero incluso si no lo son, parece ser el final de los artículos de wikipedia en conjunctive normal form, y su - aproximadamente equivalente en el mundo de probadores de imágenes automatizados - clausal normal form alter ego esbozar un algoritmo utilizable (y señalar las referencias si desea realizar esta transformación un poco más inteligente). Si necesita más que eso, cuéntenos más sobre dónde encuentra una dificultad.

Answer 2

Mira https://github.com/bastikr/boolean.py Ejemplo:

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

de salida es:

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

ACTUALIZACIÓN: Ahora prefiero esto 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

He encontré con este página: How to Convert a Formula to CNF. Muestra el algoritmo para convertir una expresión booleana a CNF en pseudo código. Me ayudó a comenzar a hablar de este tema.