SAT na teoria dos modelos finitos sem ordem

É bem conhecido na teoria dos modelos finitos que, sem uma ordem na entrada, a expressividade é muito limitada. Por exemplo, sabe-se que é igual a PSPACE , e (sem nenhuma ordem na entrada) é apenas relacional para PSPACE , uma noção definida por Abiteboul e Vianu quando provaram seu teorema: iff . (Equivalentemente P = PSPACE iff P- relacional = PSÄCE- relacional.)$FO(<,\textit{PFP})$$FO(\textit{PFP})$$FO(\textit{IFP},<)=FO(\textit{PFP},<)$$FO(\textit{IFP})=FO(\textit{PFP})$

Máquinas relacionais são máquinas de Turing com um número finito de relações. Como em um banco de dados, uma relação é um conjunto de tuplas de elementos de um universo finito. A máquina pode verificar se uma relação está vazia (se uma tabela estiver vazia), executar operações booleanas sobre as relações (união, interseção, junção, projeção) e as operações usuais da máquina de Turing. Observe que a entrada de máquinas relacionais é fornecida nas relações e não na fita. É sabido que o PSPACE- relacionais ( ) não consegue nem calcular a paridade, portanto, é menos expressivo que o PSPACE .$FO(\textit{PFP})$

Pode-se definir consultas com máquinas relacionais, mas também pode-se definir funções, sendo a resposta de uma função o conteúdo de algumas relações e a fita no final do cálculo. Tal máquina tem a propriedade de que se houver dois elementos e da entrada tal que existe um isomorfismo envio de para e para , então nunca é possível distinguir do . Em particular em todas as relações da saída, se for verdadeiro, então também será.$a$$b$$\phi$$a$$b$$b$$a$$a$$b$$R$$R(a,\overline x)$$R(b,\phi(\overline x))$

A razão para isto é que as operações permitidas (união, interseção, projeção e junção) respeitam o isomorfismo. Portanto, a saída respeita todos os isomorfismos respeitados pela entrada.

Em , e são simétricas, e a função comutação e é claramente um isomorfismo da entrada. Suponha que exista uma função para calcular atribuições satisfatórias para instâncias e cuja saída seja (o conjunto de variáveis ​​atribuídas a true em uma atribuição correta). Então nós queremos ter ou . No entanto, o isomorfismo significa que contém ambos e , ou nenhum.$(a\lor b)\land(\neg a\lor\neg b)$$a$$b$$\phi$$a$$b$$3-SAT$$P$$P=\{a\}$$P=\{b\}$$P$$a$$b$

Portanto, provamos que não existe uma função relacional do PSPACE que possa gerar uma atribuição para uma instância 3-SAT.

Minha pergunta é: como você prova que não existe um relacionamento PSPACE (ou seja, ) que aceita apenas a entrada que possui uma tarefa satisfatória? A questão é diferente, já que não pretendo calcular a tarefa e não peço para ver ou na saída, só quero ver "aceitar" ou "rejeitar". E, ao contrário do mundo usual das máquinas de Turing , não é equivalente saber se existe uma resposta e encontrar a resposta, porque não há como usar nossa máquina relacional para a pergunta "existe uma resposta com " porque não podemos diferenciar de .$FO(\textit{PFP})$$a$$b$$a=true$$a$$b$

O método padrão para mostrar resultados inexpressíveis para FO (PFP) (e para FO (LFP), por sinal) é usando o fato de que FO (PFP) está incorporado na lógica infinita de variáveis ​​finitas . Aqui é o fragmento de variável finita de , em que o último é a classe de fórmulas (infinitárias) criadas a partir dos átomos por meio de negações, disjunções e conjunções finitárias ou infinitas do tipo e , e quantificação existencial e universal. A lógica é a coleção de todas as fórmulas em$\mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}_{\infty\omega}$$\bigvee_i \phi_i$$\bigwedge_i \phi_i$$\mathrm{L}^k_{\infty\omega}$$\mathrm{L}_{\infty\omega}$que envolvem no máximo variáveis ​​(quantificadas ou não) e .$k$$\mathrm{L}^\omega_{\infty\omega} = \bigcup_k \mathrm{L}^k_{\infty\omega}$

Sabe-se que FO (PFP) (consulte o Teorema 7.4.2 no livro de Ebbinghaus e Flum "Teoria dos modelos finitos"). Portanto, se você provar que algo não é expressável em para qualquer , também provará que não é expressável em FO (PFP).$\subseteq \mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}^k_{\infty\omega}$$k$

Agora, como provar resultados inexprimíveis para ? Jogando os jogos de seixo. Estes são jogos do tipo Ehrenfeucht-Fraissé, onde o número de rodadas é ilimitado, mas cada jogador tem no máximo seixos que ele pode reutilizar (consulte Ebbinghaus e Flum no livro novamente para obter detalhes).$\mathrm{L}^k_{\infty\omega}$$k$$k$

Depois de todo esse histórico, agora podemos mostrar que o CNF-SAT não é expressável em para qualquer . Para cada fixo , precisamos encontrar uma fórmula CNF satisfatória e uma fórmula CNF insatisfatória tal que , onde significa que o Duplicador possui uma estratégia vencedora para ganhar o jogo de seixos- nas estruturas e$\mathrm{L}^k_{\infty\omega}$$k$$k$$F_k$$G_k$$F_k \equiv^k_{\infty\omega} G_k$$A \equiv^k_{\infty\omega} B$$k$$A$$B$(aqui precisamos corrigir alguma maneira sensata de codificar as fórmulas CNF como estruturas finitas: digamos que as codifiquemos como seu gráfico de incidência bipartido com elementos representando cláusulas de um lado, elementos representando variáveis ​​do outro lado e 2 tipos de relações binárias indicando quais variáveis ​​aparecem em quais cláusulas e sob qual sinal). Eu afirmo que uma escolha explícita de e é possível. Mas, em vez disso, darei uma prova indireta.$F_k$$G_k$

É trivial ver que , onde denota o gráfico de clique em vértice. Em particular, EVENNESS não é definível em . Também é sabido que o CNF-SAT é NP-completo sob reduções de primeira ordem (ver Teorema 7.16 no livro "Complexidade Descritiva" de Immerman). Como trivialmente EVENNESS está em NP, isso significa que há uma redução de primeira ordem de EVENNESS para CNF-SAT. Como reduções de primeira ordem (na lógica pura de primeira ordem, sem ordem linear embutida ou qualquer coisa como é o caso do Teorema 7.16 do livro de Immerman) preservam a expressibilidade em$K_k \equiv^k_{\infty\omega} K_{k+1}$$K_a$$a$$\mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}^\omega_{\infty\omega}$de trás para frente, o resultado é o seguinte: se o CNF-SAT fosse expressável, EVENNESS também seria; uma contradição.