Evaluaciones de Complejidad para Fragmentos Decidibles de la Teoría de Conjuntos. IV: Una Reducción Cuadrática de Restricciones sobre Conjuntos Anidados a Fórmulas Booleanas

Como contribución al razonamiento automatizado en la teoría de conjuntos, se propone una traducción de conjunciones de literales de las formas x=y∖z, x≠y∖z, y z=x, donde x, y, z representan variables que abarcan el universo de conjuntos de von Neumann, en fórmulas Booleanas sin cuantificadores de una forma normal conjuntiva bastante simple. Las fórmulas en el lenguaje objetivo involucran variables que abarcan un anillo Booleano de conjuntos, junto con un operador de diferencia y reladores que designan igualdad, no-disjunción e inclusión. Además, el resultado de cada traducción es una conjunción de literales de las formas x=y∖z y x≠y∖z y de implicaciones cuyos antecedentes son literales aislados y cuyos consecuentes son inclusiones (estrictas o no estrictas) entre variables, o igualdades entre variables. Aparte de reflejar una semántica simple y natural, que asegura la preservación de satisfacibilidad, la traducción propuesta tiene una complejidad algorítmica de tiempo cuadrático y conecta dos lenguajes, ambos conocidos por tener un problema de satisfacibilidad NP-completo.