Estou considerando a linguagem de todas as fórmulas lógicas proposicionais satisfatórias, SAT (para garantir que esse alfabeto seja finito, codificaríamos letras proposicionais de alguma maneira adequada [editar: as respostas apontaram que a resposta à pergunta pode não ser robusta em codificações variadas, então é preciso ser mais específico - veja minhas conclusões abaixo] ). Minha pergunta simples é
O SAT é uma linguagem livre de contexto?
Meu primeiro palpite foi que a resposta de hoje (início de 2017) deveria ser "Ninguém sabe, pois isso se refere a perguntas não resolvidas na teoria da complexidade". No entanto, isso não é realmente verdade (veja a resposta abaixo), embora também não seja completamente falso. Aqui está um breve resumo das coisas que sabemos (começando com algumas coisas óbvias).
- SAT não é regular (porque mesmo a sintaxe da lógica proposicional não é regular, devido a parênteses correspondentes)
- O SAT é sensível ao contexto (não é difícil fornecer um LBA para ele)
- SAT é NP-completo (Cook / Levin) e, em particular, decidido por TMs não determinísticas em tempo polinomial.
- O SAT também pode ser reconhecido por autômatos não-determinísticos de pilha unidirecional (1-NSA) (consulte WC Rounds, Complexidade de reconhecimento em idiomas de nível intermediário , Switching and Automata Theory, 1973, 145-158 http://dx.doi.org/ 10.1109 / SWAT.1973.5 )
- O problema da palavra para linguagens sem contexto tem sua própria classe de complexidade (consulte https://complexityzoo.uwaterloo.ca/Complexity_Zoo:C#cfl )
- , em que LOGCFL é a classe de problemas no espaço de log redutível a CFL (consultehttps://complexityzoo.uwaterloo.ca/Complexity_Zoo:L#logcfl). Sabe-se que NL ⊆ LOGCFL .
- NC 1 ⊊ PH NP LOGCFL LOGCFL
No entanto, esse último ponto ainda deixa a possibilidade de que o SAT não esteja em . Em geral, não consegui encontrar muito sobre o relacionamento de com a hierarquia que possa ajudar a esclarecer o status epistêmico da minha pergunta.CFL NC
Observação (depois de ver algumas respostas iniciais): Não estou esperando que a fórmula esteja na forma normal conjuntiva (isso não fará diferença na essência da resposta e, geralmente, os argumentos ainda se aplicam, pois um CNF também é uma fórmula. alegar que a versão do número constante de variáveis do problema é regular falha, pois é necessário parênteses para a sintaxe.).
Conclusão: Ao contrário do meu palpite inspirado na teoria da complexidade, pode-se mostrar diretamente que o SAT não é livre de contexto. A situação, portanto, é:
- Sabe-se que o SAT não é livre de contexto (em outras palavras: SAT não está em ), sob a suposição de que se use uma codificação "direta" de fórmulas nas quais variáveis proposicionais são identificadas por números binários (e alguns outros símbolos são usados para operadores e separadores).
- Não se sabe se o SAT está em , mas "a maioria dos especialistas pensa" que não, pois isso implicaria . Isso também significa que não se sabe se outras codificações "razoáveis" do SAT são livres de contexto (supondo que consideremos o espaço de log um esforço de codificação aceitável para um problema difícil de NP).P = NP
Observe que esses dois pontos não implicam . Isso pode ser mostrado diretamente, mostrando que existem idiomas em (portanto, em ) que não são livres de contexto (por exemplo, ).L LOGCFL a n b n c n
Respostas:
Apenas uma prova alternativa usando uma mistura de resultados conhecidos.
Suponha que:
Por exemplo, é escrito como: (o operador tem precedência sobre ) .φ=(x1∨x2)∧−x3 sφ=+1∨+10∧−11∈S ∨ ∧
Suponha que da fórmula correspondente seja satisfatória seja CF.L={sφ∈S∣ φ }
Se o interceptarmos com o idioma regular: , ainda temos um idioma CF. Também podemos aplicar o homomorfismo: , e o idioma permanece CF.R={+1a∧−1b∧−1c∣a,b,c>0} h(+)=ϵ h(−)=ϵ
Mas a linguagem que obtemos é: , porque se , a fórmula "source" é que não é satisfatório (da mesma forma se ). Mas é uma contradição bem conhecida da linguagem não CF .L′={1a∧1b∧1c∣a≠b,a≠c} a=b +xa∧−xa∧−xb a=c L′ ⇒
fonte
Se o número de variáveis é finito, o mesmo ocorre com o número de conjunções satisfatórias; portanto, sua linguagem SAT é finita (e, portanto, regular). [Editar: esta reivindicação assume o formulário CNFSAT.]
Caso contrário, vamos concordar em codificar fórmulas como por . Usaremos o lema de Ogden para provar que a linguagem de todas as conjunções satisfatórias não é livre de contexto.(x17∨¬x21)∧(x1∨x2∨x3) (17+~21)(1+2+3)
Seja a constante de "marcação" no lema de Ogden e considere uma fórmula sat cuja primeira cláusula consiste em - ou seja, a codificação de , onde é o número decimal que consiste em uns. Marcamos os de e exigimos que todos os bombeamentos da decomposição apropriada de (veja a conclusão do lema de Ogden) também sejam satisfatórios. Mas podemos facilmente bloquear isso exigindo que nenhuma cláusula contenha , onde é uma sequência de menor quew ( 1 p ) ( x N ) N p p 1 p w x q q 1 p w x q wp w (1p) (xN) N p p 1p w xq q 1 p , seja satisfatório - por exemplo, garantindo que todas as outras cláusulas de tenham uma negação de cada um desses . Isso significa que falha na propriedade "bombeamento negativo" e concluímos que o idioma não é livre de contexto. [Nota: eu ignorei os casos triviais em que o bombeamento produz cordas mal formadas.]w xq w
fonte