Tarefa para tornar a fórmula insatisfatória

8

Vamos imaginar que temos uma fórmula satisfatóriaF(A0,A1,...Ak,S0,...,Sn) O problema a ser resolvido é "Existe uma atribuição para variáveis (S0,...,Sn) o que tornará F insatisfatório? ". Uma maneira de resolver é encontrar todas as soluções para F em termos de variáveis S0,...,Sn e se a contagem for < 2n, a solução que falta será a resposta, mas a complexidade desse algoritmo é enorme, se o número dessas atribuições for pequeno.

Minhas perguntas são:

  • Existe uma maneira de resolver o problema com menos chamadas para o SAT Solver?
  • É um problema bem conhecido na teoria (o que eu deveria pesquisar no google)?
Grigor Aghanyan
fonte
1
"o que tornará F insatisfatório" - isso não faz sentido. Você quer dizer simplesmente "não satisfaz F"? Então você está falando sobre o problema TAUTOLOGY (resp. É complemento).
Raphael
Ignorando o fato de que a pergunta não faz sentido, acho que tentando encontrar uma solução para ¬F(UMA0 0,UMA1,,UMAk,S0 0,,Sn)pode ser o que você está procurando.
Dave Clarke
Talvez eu não estivesse claro. Após aplicar as atribuições para(S0 0,...,Sn) teremos outra fórmula G(UMA0 0,...,UMAk) e isso deve ser insatisfatório.
Grigor Aghanyan

Respostas:

6

Seu problema é o canônico Σ2Pproblema completo:

SUMA¬F(UMA,S).
Como tal, acredita-se ser mais difícil que o SAT (que é Σ1P) Resolvê-lo com algumas chamadas SAT-oracle é semelhante a resolver o SAT de maneira eficiente (a questão P vs. NP), embora possa ser queΣ2P=Σ1P enquanto PNP, portanto, em certo sentido, há mais esperança para o seu problema do que para o próprio SAT.
Yuval Filmus
fonte
Exatamente. Obrigado pela resposta. Então a solução com2nsolucionador de chamadas "não é uma solução ruim" para isso? Alguns links para artigos sobre esse problema me ajudarão bastante.
Grigor Aghanyan
Na prática, pode haver heurísticas que funcionem bem em alguns problemas, mas não conheço nenhum. A hierarquia polinomial (que contémΣ2P) deve ser abordada em qualquer livro didático sobre complexidade computacional.
Yuval Filmus
4

Esse é um problema conhecido: é o problema do 2QBF. Infelizmente, é significativamente mais difícil que o SAT. Existem solucionadores QBF disponíveis. Você pode tentar encontrar um solucionador de QBF (ou, melhor ainda, um solucionador de 2QBF) e ver se ele pode resolver sua fórmula. No entanto, os solucionadores de QBF não escalam tão bem quanto os solucionadores de SAT; O QBF é significativamente mais difícil que o SAT.

Consulte https://cstheory.stackexchange.com/q/11022/5038 e http://www.qbflib.org/ para obter alguns recursos que podem ser úteis.

DW
fonte