Como provar que uma versão restrita do 3SAT, na qual nenhum literal pode ocorrer mais de uma vez, é solucionável em tempo polinomial?

10

Estou tentando elaborar uma tarefa (tirada do livro Algoritmos - de S. Dasgupta, CH Papadimitriou e UV Vazirani , Cap 8, problema 8.6a), e estou parafraseando o que afirma:

Dado que o 3SAT permanece NP-completo, mesmo quando restrito a fórmulas nas quais cada literal aparece no máximo duas vezes, mostre que, se cada literal aparecer no máximo uma vez, o problema será resolvido no tempo polinomial.

Tentei resolver isso separando as cláusulas em vários grupos:

  1. Cláusulas que não tinham nenhuma variável em comum com o restante das cláusulas
  2. Cláusulas que tinham apenas 1 variável em comum
  3. Cláusulas que tinham 2 variáveis ​​em comum
  4. Cláusulas que tinham todas as 3 variáveis ​​em comum

Meu raciocínio foi tentado de acordo com o argumento de que o número de tais grupos é finito (devido à restrição imposta de nenhum literal estar presente mais de uma vez), e poderíamos tentar satisfazer primeiro o grupo mais restrito (grupo 4) e depois substituir o resultam em grupos restritos menores (3, 2 e depois 1), mas percebi que isso não estava me levando a lugar nenhum, pois isso não difere muito do caso da versão restrita do 3SAT na qual cada literal pode aparecer no máximo duas vezes, comprovadamente NP-completo.

Tentei pesquisar online por quaisquer dicas / soluções, mas tudo o que consegui foi esse link , no qual a dica declarada não fazia sentido suficiente para mim, e estou reproduzindo literalmente aqui:

xEuCjxEuxEu¯CkCjCk¯

CjCkCjCk¯CjCk¯

Qualquer ajuda para descriptografar a dica ou fornecer um caminho que eu possa explorar seria realmente apreciada.

TCSGrad
fonte

Respostas:

12

Sem perda de generalidade, podemos assumir que cada variável aparece exatamente uma vez positiva e exatamente uma vez negativamente (se uma variável aparecer apenas uma vez defina seu valor para satisfazer a cláusula e remover a cláusula). Também podemos assumir que uma variável não aparece em uma cláusula mais de uma vez (se uma variável aparecer positiva e negativamente em uma cláusula, a cláusula é satisfeita e pode ser removida). Isso não altera a satisfação.

Agora use a regra de resolução para eliminar as variáveis ​​uma a uma (uma vez que cada variável aparece exatamente uma vez positivamente e uma vez negativamente, esse é um processo determinístico). Se a qualquer momento obtivermos a cláusula vazia, o conjunto de cláusulas é insatisfatório, caso contrário, é satisfatório. Isto é porque:

  • resolução é um sistema completo de prova proposicional (ou seja, se uma cláusula é logicamente implícita pelo conjunto de cláusulas, é derivável do conjunto de cláusulas usando apenas a regra de resolução),

  • um conjunto de cláusulas é insatisfatório se implicar logicamente a cláusula vazia.

(xB)(x¯C))(BC), que possui uma cláusula a menos do que antes da resolução. Por outro lado, se você aplicou isso a uma fórmula 3SAT sem restrição ao número de aparências de cada literal, aplicar a resolução pode fazer com que o número de cláusulas aumente exponencialmente.

Kaveh
fonte
3
umaB¬umaCBC
11
Também é necessário garantir que a invariante ainda se aplique após o uso da resolução. Após essa etapa, a instância SAT (observe, não é mais 3SAT) mantém a propriedade de que todo literal ocorre precisamente uma vez positivamente e uma vez negativamente. Isso também mostra que a restrição 3SAT na questão não era necessária; A resolução da unidade funciona para qualquer instância SAT que satisfaça a restrição de grau 2. Em resumo: a resolução da unidade resolve o grau 2 SAT em tempo linear.
András Salamon
Eu não entendo a última parte. Por que as cláusulas aumentam exponencialmente no 3SAT normal?
Parth Tamane 18/11/19