Conversión entre k-SAT y XOR-SAT

8

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.2norte-1nortek

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.kk

Omar Shehab
fuente
55
¿No es claramente imposible en el peor de los casos? Algunas fórmulas CNF no son afines, por lo que no pueden representarse como una conjunción de cláusulas XOR.
Tsuyoshi Ito
1
En particular, no tiene una fórmula XOR-SAT equivalente. Xy
Huck Bennett el
@ TsuyoshiIto, de acuerdo. Creo que debería haber asumido la promesa de que las expresiones -SAT tienen expresiones XOR-SAT equivalentes. Actualizando la pregunta. k
Omar Shehab
@HuckBennett, agregué una promesa en la pregunta.
Omar Shehab
1
Ya veo, ¡eso hace que el problema sea interesante!
Tsuyoshi Ito

Respuestas:

6

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.unasiunasi

En el caso limitado de recuperar relaciones XOR codificadas de la manera habitual, es decir

unasiC

a

¬unasiCuna¬siCunasi¬C¬una¬si¬C

Esto se puede hacer en tiempo polinómico clasificando las cláusulas seguidas de una exploración de tiempo lineal.

Kyle Jones
fuente
Gracias. Me gustaría saber la complejidad de convertir una expresión CNF en una expresión XOR-SAT. Supongo que estamos considerando aquellas expresiones CNF para las que hay expresiones XOR-SAT equivalentes.
Omar Shehab
¿Podemos decir que el algoritmo Davis-Putnam-Logemann-Loveland es, con mucho, el resultado más conocido para esto?
Omar Shehab el
2
A menos que NP = RP (un resultado milagroso) adivinar las relaciones XOR requerirá tiempo exponencial en el caso general. Esto es independiente del algoritmo de resolución SAT utilizado.
Kyle Jones
¿ implica P = N P ? PAGS=UPAGSPAGS=nortePAGS
rus9384
@ rus9384 No necesariamente. Ver Si uno muestra que UN-k-SAT está en P, ¿implica P = NP?
Kyle Jones