¿El XOR-SAT generalizado tiene solución eficiente?

12

He visto cómo XOR-3-SAT se puede resolver de manera eficiente (por ejemplo, consulte la sección "Satisfacción de XOR" en la entrada de Wikipedia para el problema de satisfacción booleana ).

Me pregunto una pregunta básica: ¿es XOR-k-SAT eficientemente solucionable, para fórmulas con cantidades variables de literales por cláusula?

Realmente me gustaría saber si podemos aumentar la cantidad de literales por cláusula más allá de 3, y si podemos tener longitudes de cláusula mixtas.

complexity-theory satisfiability Matt Groff
fuente
2
¿Qué investigación has hecho? Esperamos que haga un esfuerzo serio por su cuenta primero, antes de preguntar, y que nos muestre en la pregunta qué investigación ha hecho y qué ha intentado. Wikipedia menciona que el algoritmo para resolver XOR-3-SAT es la eliminación gaussiana. ¿Ha intentado comprender cómo funciona eso y ver si se aplica a XOR-k-SAT?
DW
@DW Admito que no hice mucha investigación al respecto. Vi la mención de la eliminación gaussiana, y pensé que esto funcionaría para XOR-SAT generalizado. Pero supongo que estaba buscando confirmación. Espero que perdones mi pereza. Intentaré investigar más en el futuro, antes de hacer preguntas como esta.
Matt Groff el

Respuestas:

11

Parece que el artículo de Wikipedia al que se vinculó dice que XORSAT (no solo 3-XORSAT) está en P. El método por el cual están resolviendo esa fórmula de 3-XORSAT en su ejemplo se generaliza muy fácilmente a fórmulas en las que las cláusulas pueden tener arbitrariamente gran número de variables y diferentes números de variables.

Simplemente mira la fórmula como un sistema de ecuaciones lineales donde tiene una ecuación para cada cláusula y una variable para cada variable. Por ejemplo, la fórmula:

(x1⊕x2⊕¬x3⊕x5)∧(x2⊕x3)

tiene una asignación satisfactoria si y solo si el siguiente sistema de ecuaciones tiene una solución:

x1+x2+(1+x3)+x5≡1mod2
x2+x3≡1mod2

¡Y podemos encontrar soluciones a sistemas lineales de ecuaciones como estas en tiempo polinómico usando la eliminación gaussiana!

Dylan McKay
fuente
6

Si. Es solucionable por eliminación gaussiana. La eliminación gaussiana puede resolver cualquier sistema de ecuaciones que sea un módulo lineal. XOR actúa como módulo de suma 2, por lo que cada cláusula XOR-SAT actúa como un módulo de ecuación lineal 2. En consecuencia, la eliminación gaussiana puede resolver cualquier fórmula XOR-k-SAT o cualquier fórmula XOR-SAT, incluso si hay un número variable de literales por cláusula o longitudes de cláusula mixta, en tiempo polinómico.

DW
fuente