Tarefa para tornar a fórmula insatisfatória

8

Vamos imaginar que temos uma fórmula satisfatória $F(A_0, A_1,...A_k,S_0,...,S_n)$ O problema a ser resolvido é "Existe uma atribuição para variáveis $(S_0,...,S_n)$ o que tornará F insatisfatório? ". Uma maneira de resolver é encontrar todas as soluções para F em termos de variáveis $S_0,...,S_n$ e se a contagem for < $2^n$ , 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)?

logic satisfiability sat-solvers 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

\neg F (A_{0}, A_{1}, \dots, A_{k}, S_{0}, \dots, S_{n})

$\neg F(A_0,A_1,\ldots, A_k,S_0,\ldots, S_n)$ pode ser o que você está procurando.

Dave Clarke

Talvez eu não estivesse claro. Após aplicar as atribuições para

(S_{0}, . . ., S_{n})

$(S_0,...,S_n)$ teremos outra fórmula

G (A_{0}, . . ., A_{k})

$G(A_0 ,..., A_k)$ e isso deve ser insatisfatório.

Grigor Aghanyan

6

Seu problema é o canônico $\Sigma_2^P$ problema completo:

\exists \vec{S} \forall \vec{UMA} \neg F (\vec{UMA}, \vec{S}) .

$\exists \vec{S} \forall \vec{A} \lnot F(\vec{A},\vec{S}).$ Como tal, acredita-se ser mais difícil que o SAT (que é

Σ_{1}^{P}

$\Sigma_1^P$ ) 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

Σ_{2}^{P} = Σ_{1}^{P}

$\Sigma_2^P = \Sigma_1^P$ enquanto

P \neq N P

$P \neq NP$ , 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 com

2^{n}

$2^n$ solucionador 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

Σ_{2}^{P}

$\Sigma_2^P$ ) 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

Tarefa para tornar a fórmula insatisfatória

Respostas: