Verifique a correção da eliminação do quantificador, usando SAT

Seja e sejam vetores de variáveis ​​booleanas. Eu tenho um predicado booleano em . Dou à minha amiga Priscilla . Em resposta, ela me fornece , um predicado booleano em , e ela afirma que$x=(x_1,\dots,x_n)$$y=(y_1,\dots,y_n)$$n$$Q(x,y)$$x,y$$Q(x,y)$$P(x)$$x$

ou em outras palavras, que

Eu gostaria de verificar sua reivindicação de alguma forma. Como a Priscilla pode me ajudar a verificar esta reivindicação?

Você pode assumir que e são representados como fórmulas CNF e que não são muito grandes (tamanho polinomial ou algo assim).$P$$Q$

Em um mundo ideal, seria incrível se eu pudesse reduzir o problema de verificação dessa reivindicação para SAT: eu tenho um solucionador de SAT e seria ótimo se eu pudesse usar o solucionador de SAT para verificar essa reivindicação. No entanto, tenho certeza de que não será possível formular o problema de verificar essa afirmação diretamente como uma instância SAT; testar a validade de uma fórmula 2QBF é quase certamente mais difícil que o SAT. (A direção é fácil de formular como uma instância SAT, mas a direção é difícil porque envolve inerentemente dois quantificadores alternativos.)$\Leftarrow$$\Rightarrow$

Mas suponha que Priscilla possa me dar alguma evidência adicional para apoiar sua afirmação. Existe alguma evidência adicional ou testemunha que Priscilla possa me dar, o que facilitaria a verificação de sua alegação? Em particular, há alguma evidência ou testemunha adicional que ela poderia me dar, o que facilitaria a formulação do problema de verificação de sua reivindicação como uma instância do SAT (na qual eu posso aplicar meu solucionador SAT)?

Um aspecto incomum da minha configuração é que estou assumindo (heuristicamente) que tenho um oráculo para o SAT. Se você gosta da teoria da complexidade, pode pensar assim: Estou assumindo o papel de uma máquina que pode computar coisas em (ou seja, em ), e estou procurando verificar se Priscilla está declaração usando um algoritmo em . Meus agradecimentos à MDX por essa maneira de pensar sobre as coisas.$P^{NP}$$\Delta^P_2$$P^{NP}$

Minha motivação / aplicação: estou procurando fazer a verificação formal de um sistema (por exemplo, verificação de modelo simbólico), e uma etapa fundamental no raciocínio envolve a eliminação do quantificador (ou seja, começando com , obtenha ). Espero alguma maneira limpa de verificar se a eliminação do quantificador foi feita corretamente.$Q$$P$

Se não houver uma solução que funcione para todos os possíveis fique à vontade para sugerir uma solução "sólida, mas não completa", ou seja, uma técnica que, para muitos permita-me verificar a equivalência reivindicada. (Mesmo que ele não verifique a reivindicação em alguns que satisfazem a reivindicação, ainda posso tentar isso como uma heurística, desde que nunca afirme inadequadamente ter verificado uma declaração falsa. Em qualquer , pode funcionar ou não; se não funcionar, não estou pior do que onde comecei.)$P,Q$$P,Q$$P,Q$$P,Q$

Aqui estão duas técnicas que eu consegui identificar:

• Identifique uma função Skolem explícita. Suponha que Priscilla possa identificar uma função explícita$f$ de tal modo que

  $$\forall x . P(x) \Leftrightarrow Q(x,f(x))$$

  detém. Daí decorre que a afirmação de Priscilla está correta.

  Isso significa que Priscilla pode nos ajudar a verificar sua reivindicação, fornecendo uma função $f$para que a proposição acima se mantenha. Podemos confirmar que a proposição acima é válida testando a seguinte fórmula para garantir a satisfação:

  $$\neg (P(x) \Leftrightarrow Q(x,f(x))).$$

  Se essa fórmula não for satisfatória, a reivindicação de Priscilla foi verificada.

  Uma ressalva é que Priscilla precisa ser capaz de identificar uma função adequada $f$. Uma ressalva adicional é que precisamos$f$ser concretamente representável de alguma forma concisa, digamos, como um circuito booleano de tamanho polinomial. No entanto, se essas condições forem atendidas, essa técnica deve funcionar.

• Um argumento híbrido. Considere o caso especial desse problema, em que estamos quantificando sobre uma variável de um bit (em vez de uma$n$variável de bits); Acontece que o problema é fácil de resolver nesse caso. Isso sugere que tentamos encadear essa técnica$n$ vezes, cada vez que remover mais um pedaço $y$. Acontece que essa ideia às vezes funciona, mas nem sempre.

  Deixe-me explicar como verificar a alegação de Priscilla no caso em que $y=(y_1)$é uma variável de um bit. Então$\exists y . Q(x,y)$ é equivalente a $Q(x,\text{False}) \lor Q(x,\text{True})$. A última fórmula é no máximo duas vezes maior que$Q$, de tamanho ainda polinomial. Agora podemos usar nosso solucionador SAT para testar se$Q(x,\text{False}) \lor Q(x,\text{True})$ é equivalente a $P(x)$; a equivalência vale exatamente se a seguinte fórmula não for satisfatória:

  $$\neg (P(x) \Leftrightarrow (Q(x,\text{False}) \lor Q(x,\text{True}))).$$

  Portanto, se estivermos quantificando em um único bit, isso permitirá verificar se a eliminação do quantificador foi feita corretamente.

  Para resolver o problema original, aplique isso várias vezes. O trabalho de Priscilla será nos dar$n+1$ predicados booleanos $R_0,R_1,R_2,\dots,R_n$ de tal modo que

  $$R_i(x,(y_{i+1},\dots,y_n)) \equiv \exists y_1,y_2,\dots,y_i . Q(x,y).$$

  Nossa tarefa será verificar se todos esses predicados booleanos foram gerados corretamente. Podemos fazer isso testando se$Q(x,y) \equiv R_0(x,y)$, $P(x) \equiv R_n(x)$,

  $$R_{i+1}(x,(y_{i+2},\dots,y_n)) \equiv \exists y_{i+1} . R_i(x,(y_{i+1},\dots,y_n)) \qquad \text{for $i=1,2,\dots,n-1$}.$$

  Observe que o último é uma instância de eliminação do quantificador com um único bit; portanto, já descrevemos como testá-lo corretamente usando um solucionador SAT. Também podemos testar se$Q \equiv R_0$ e $P \equiv R$usando um solucionador SAT diretamente. Então, podemos verificar se Priscilla gerou$R_0,\dots,R_n$corretamente. Se ela fez, então verificamos que$P$ foi gerado adequadamente.

  Uma ressalva é que Priscilla precisa ser capaz de gerar o $R_i$'s. Uma ressalva maior é que o tamanho de todo o$R_i$precisa ser razoável (digamos, de tamanho polinomial). Se Priscilla gerar o$R_i$ingenuamente, seu tamanho pode crescer exponencialmente com $i$, o que não é bom. Portanto, Priscilla precisará de uma maneira de simplificar a cada estágio; precisa existir alguma sequência de$R_0,\dots,R_n$todos com tamanho polinomial, e Priscilla precisa ser capaz de encontrar essa sequência. Isso não é de forma alguma garantido. Dito isto, se Priscilla puder fazer isso, essa técnica deve funcionar.

Não estou totalmente satisfeito com essas técnicas - elas são heurísticas incompletas e podem falhar em algumas / muitas instâncias de problemas -, portanto, eu ainda estaria interessado em ver outras maneiras de abordar esse problema.