¿Existe un algoritmo (eficiente) para determinar si una ecuación de dos términos en el lenguaje de los operadores elementales de la teoría de conjuntos es una identidad?

Question

Por operaciones elementales de la teoría de conjuntos me refiero a las que se suelen imaginar en los diagramas de Venn: unión, intersección, diferencia de conjuntos, etc. En la formulación de mi pregunta he incluido la palabra "eficiente" entre paréntesis porque en la complejidad computacional este término se utiliza con diferentes significados y aquí no estoy muy interesado en la complejidad. Me gustaría conocer cualquier algoritmo que no se limitara a "agotar todas las posibilidades" (como la sustitución de 0s y 1s, en el caso de los términos booleanos), un algoritmo que fuera útil o instructivo cuando se implementara como programa informático.

Esta pregunta vino naturalmente después de otra pregunta mía: ¿Es decidible la teoría ecuacional de las álgebras booleanas generalizadas?

Answer 1

Como complemento a la respuesta de Andreas Blass, una buena referencia es Fascículo 6 del volumen 4 de Don Knuth Arte de la programación informática que está dedicado a la Satisfacción. En pocas palabras, la mayoría de los algoritmos SAT proposicionales pueden dividirse en dos clases: algoritmos basados en paseos aleatorios y algoritmos de aprendizaje de cláusulas basados en conflictos (CDCL).

Estos algoritmos han progresado constantemente en las dos últimas décadas. Los algoritmos CDCL, en particular, tienen muchas aplicaciones prácticas y son capaces tanto de demostrar como de refutar la satisfabilidad. De hecho, producen pruebas de resolución en el último caso. (A veces estas pruebas son bastante grande .)

No es raro que estos solucionadores de SAT decidan instancias de problemas con cientos de miles de variables proposicionales y millones de cláusulas. Su tiempo de ejecución en el peor de los casos sigue siendo exponencial, y a veces se ven sorprendidos por casos de problemas mucho más pequeños. Aun así, desde el punto de vista de la ingeniería son pequeñas maravillas y definitivamente merecen tu atención. El código fuente está disponible para algunas de las mejores herramientas como lingeling o glucosa .

Answer 2

La teoría que describes es decidible, por el algoritmo que mencionas pero no quieres, es decir, sustituyendo 0's y 1's de todas las formas posibles. De hecho, decidir si una ecuación booleana (usando $\cap,\cup,-$ ) es una identidad equivale a decidir si una fórmula en lógica proposicional es una tautología. Que esto pueda hacerse en tiempo polinómico es un gran problema abierto (el problema P=NP). Sin embargo, se sabe mucho sobre algoritmos que, en muchos casos, funcionan mucho mejor que el algoritmo del enchufe 0 y 1. En particular, la gente ha programado heurísticas para adivinar qué combinaciones de 0's y 1's es probable que den contraejemplos. No soy un experto en estos métodos, pero hasta que aparezca un experto y te dé una respuesta mejor, podrías buscar en Google "SAT-solvers" y encontrar una buena cantidad de información. ("SAT" se refiere al problema de decidir si una fórmula en lógica proposicional es satisfacible; eso es equivalente a preguntar si la negación de la fórmula no es una tautología, así que es esencialmente la misma pregunta para tus propósitos).