O XOR-SAT generalizado é eficientemente solucionável?

12

Vi como o XOR-3-SAT é eficientemente solucionável (por exemplo, consulte a seção "XOR-satisfability" na entrada da Wikipedia para o problema de satisfação booleana ).

Estou pensando em uma pergunta básica: O XOR-k-SAT é eficientemente solucionável, para fórmulas com quantidades variáveis ​​de literais por cláusula?

Eu realmente gostaria de saber se podemos aumentar a quantidade de literais por cláusula além de 3 e se podemos ter comprimentos de cláusulas mistos.

complexity-theory satisfiability Matt Groff
fonte
2
Que pesquisa você fez? Esperamos que você faça um esforço sério primeiro, antes de perguntar, e nos mostre na pergunta quais pesquisas você fez e o que tentou. A Wikipedia menciona que o algoritmo para resolver o XOR-3-SAT é a eliminação gaussiana. Você tentou entender como isso funciona e ver se isso se aplica ao XOR-k-SAT?
DW
@DW Admito que não fiz muita pesquisa sobre isso. Vi a menção à eliminação gaussiana e imaginei que isso funcionaria para o XOR-SAT generalizado. Mas acho que estava procurando por confirmação. Espero que você perdoe minha preguiça. Vou tentar fazer mais pesquisas no futuro, antes de fazer perguntas como essa.
precisa

Respostas:

11

Parece que o artigo da Wikipedia ao qual você vinculou diz que XORSAT (não apenas 3-XORSAT) está em P. O método pelo qual eles estão resolvendo a fórmula 3-XORSAT em seu exemplo generaliza muito facilmente as fórmulas nas quais as cláusulas podem ter arbitrariamente grande número de variáveis ​​e números diferentes de variáveis.

Você apenas vê a fórmula como um sistema de equações lineares, onde você tem uma equação para cada cláusula e uma variável para cada variável. Por exemplo, a fórmula:

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

tem uma atribuição satisfatória se e somente se o seguinte sistema de equações tiver uma solução:

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

E podemos encontrar soluções para sistemas lineares de equações como estas em tempo polinomial usando a eliminação gaussiana!

Dylan McKay
fonte
6

Sim. É solucionável por eliminação gaussiana. A eliminação gaussiana pode resolver qualquer sistema de equações que seja módulo linear. XOR atua como módulo de adição 2, portanto, cada cláusula XOR-SAT atua como módulo de equação linear 2. Consequentemente, a eliminação gaussiana pode resolver qualquer fórmula XOR-k-SAT ou qualquer fórmula XOR-SAT, mesmo se houver um número variável de literais por cláusula ou comprimento de cláusula mista, em tempo polinomial.

DW
fonte