De acuerdo con el Módulo XOR Satisfiability Solver para la integración DPLL por Tero Laitinen, necesitamos cláusulas CNF para convertir una cláusula XOR-SAT literal si no queremos aumentar el número de literales. Entonces, entiendo que el costo computacional para convertir una expresión XOR-SAT en un estrictamente CNF -SAT es exponencial.
Mi pregunta: ¿Cuál es el costo computacional si quiero revertir el proceso? ¿Cuál es el costo computacional de convertir una expresión CNF -SAT en una XOR-SAT? Asumo la promesa de que en este caso solo se consideran las expresiones -SAT con expresiones XOR-SAT equivalentes.
sat
boolean-functions
boolean-formulas
Omar Shehab
fuente
fuente
Respuestas:
Si todas las relaciones XOR entre variables en las fórmulas de CNF pudieran detectarse en tiempo polinomial, esto permitiría la solución de UNAMBIGUOUS-SAT en tiempo polinomial. Según el teorema de Valiant-Vazirani, este resultado implicaría que NP = RP.
Para resolver UNAMBIGUOUS-SAT, recuerde que implica a ≠ b . Encuentre la relación XOR entre cada par de variables y use los resultados para dividir las variables en dos grupos de variables equivalentes. Una vez hecho esto, solo se requieren dos tareas de prueba para determinar la satisfacción.a ⊕ b a ≠ b
En el caso limitado de recuperar relaciones XOR codificadas de la manera habitual, es decir
a
Esto se puede hacer en tiempo polinómico clasificando las cláusulas seguidas de una exploración de tiempo lineal.
fuente