Conversão entre k-SAT e XOR-SAT

8

De acordo com o XOR Satisfiability Solver Module para integração de DPLL por Tero Laitinen, precisamos de cláusulas n - 1 CNF para converter uma cláusula XOR-SAT n literal se não quisermos aumentar o número de literais. Portanto, entendo que o custo computacional para converter uma expressão XOR-SAT em um estritamente CNF k- SAT é exponencial.2n1nk

Minha pergunta: qual é o custo computacional se eu quiser reverter o processo? Qual é o custo computacional da conversão de uma expressão CNF -SAT em uma expressão XOR-SAT? Assumo a promessa de que, neste caso, apenas as expressões k -SAT com expressões XOR-SAT equivalentes são consideradas.kk

Omar Shehab
fonte
5
Não é claramente impossível no pior dos casos? Algumas fórmulas CNF não são afins, portanto, não podem ser representadas como uma conjunção de cláusulas XOR.
Tsuyoshi Ito
1
Em particular, não possui fórmula XOR-SAT equivalente. xy
Huck Bennett
@TsuyoshiIto, concordou. Acho que deveria ter assumido a promessa de que as expressões -SAT têm expressões XOR-SAT equivalentes. Atualizando a pergunta. k
Omar Shehab
@ HuckBennett, adicionei uma promessa à pergunta.
Omar Shehab
1
Entendo, isso torna o problema interessante!
Tsuyoshi Ito

Respostas:

6

Se todos os relacionamentos XOR entre variáveis ​​nas fórmulas CNF pudessem ser detectados em tempo polinomial, isso permitiria a solução de UNAMBIGUOUS-SAT em tempo polinomial. Pelo teorema de Valiant – Vazirani, esse resultado implicaria que NP = RP.

abab

No caso limitado de recuperar relações XOR codificadas da maneira usual, ou seja,

abc

para

¬abca¬bcab¬c¬a¬b¬c

isso pode ser feito em tempo polinomial , classificando as cláusulas seguidas por uma varredura em tempo linear.

Kyle Jones
fonte
obrigado. Gostaria de saber a complexidade de converter uma expressão CNF em uma expressão XOR-SAT. Suponho que estamos considerando as expressões CNF para as quais existem expressões XOR-SAT equivalentes.
Omar Shehab
Podemos dizer que o algoritmo Davis-Putnam-Logemann-Loveland é de longe o resultado mais conhecido para isso?
Omar Shehab
2
A menos que NP = RP (um resultado milagroso) que divida as relações XOR exija tempo exponencial no caso geral. Isso é independente do algoritmo de solução SAT usado.
Kyle Jones
P=UPP=NP
@ rus9384 Não necessariamente. Veja Se alguém mostra que UNIQUE k-SAT está em P, isso implica P = NP?
Kyle Jones