Satisfabilidade - Satisfiability

Na lógica matemática , incluindo, em particular, a lógica de primeira ordem e o cálculo proposicional , satisfatibilidade e validade são conceitos elementares da semântica . Uma fórmula é satisfatória se houver uma interpretação ( modelo ) que torne a fórmula verdadeira. Uma fórmula é válida se todas as interpretações a tornarem verdadeira. Os opostos desses conceitos são a insatisfação e a invalidade , ou seja, uma fórmula é insatisfatória se nenhuma das interpretações torna a fórmula verdadeira, e inválida se alguma dessas interpretações torna a fórmula falsa. Estes quatro conceitos estão relacionados uns aos outros de uma maneira exatamente análoga à Aristóteles 's quadrado de oposição .

Os quatro conceitos podem ser levantados para serem aplicados a teorias inteiras : uma teoria é satisfatória (válida) se uma (todas) das interpretações tornam cada um dos axiomas da teoria verdadeiro, e uma teoria é insatisfatória (inválida) se todos (uma) das interpretações faz com que um dos axiomas da teoria seja falso.

Também é possível considerar apenas interpretações que tornam verdadeiros todos os axiomas de uma segunda teoria. Essa generalização é comumente chamada de teorias do módulo de satisfatibilidade .

A questão de saber se uma sentença na lógica proposicional é satisfatória é um problema decidível ( problema de satisfatibilidade booleana ). Em geral, a questão de saber se uma sentença de lógica de primeira ordem pode ser satisfeita não é decidível. Na álgebra universal e na teoria equacional , os métodos de reescrita de termos , fechamento de congruência e unificação são usados ​​para tentar decidir a satisfatibilidade. Se uma determinada teoria é decidível ou não, depende se a teoria é livre de variáveis ou está em outras condições.

Redução de validade para satisfatibilidade

Para lógicas clássicas com negação, é geralmente possível reexpressar a questão da validade de uma fórmula para uma que envolve satisfatibilidade, por causa das relações entre os conceitos expressos no quadrado de oposição acima. Em particular, φ é válido se e somente se ¬φ for insatisfatório, o que significa que é falso que ¬φ seja satisfatório. Dito de outra forma, φ é satisfatório se e somente se ¬φ for inválido.

Para lógicas sem negação, como o cálculo proposicional positivo , as questões de validade e satisfatibilidade podem não estar relacionadas. No caso do cálculo proposicional positivo , o problema da satisfatibilidade é trivial, pois toda fórmula é satisfazível, enquanto o problema da validade é co-NP completo .

Satisfatibilidade proposicional para lógica clássica

No caso da lógica proposicional clássica , a satisfatibilidade é decidível para fórmulas proposicionais. Em particular, satisfatibilidade é um problema NP-completo , e é um dos problemas mais intensamente estudados na teoria da complexidade computacional .

Satisfação na lógica de primeira ordem

Para a lógica de primeira ordem (FOL), a satisfatibilidade é indecidível . Mais especificamente, é um problema co-RE-completo e, portanto, não semidecidível . Esse fato tem a ver com a indecidibilidade do problema de validade para FOL. A questão do status do problema de validade foi colocada primeiramente por David Hilbert , como o chamado Entscheidungsproblem . A validade universal de uma fórmula é um problema semidecidível pelo teorema da completude de Gödel . Se a satisfatibilidade também fosse um problema semidecidível, então o problema da existência de contra-modelos também o seria (uma fórmula tem contra-modelos se sua negação for satisfazível). Portanto, o problema de validade lógica seria decidível, o que contradiz o teorema de Church-Turing , um resultado que afirma a resposta negativa para o Entscheidungsproblem.

Satisfabilidade na teoria do modelo

Na teoria do modelo , uma fórmula atômica é satisfatória se houver um conjunto de elementos de uma estrutura que torne a fórmula verdadeira. Se A é uma estrutura, φ é uma fórmula, e a é uma coleção de elementos, retirados da estrutura, que satisfazem φ, então é comumente escrito que

A ⊧ φ [a]

Se φ não tem variáveis ​​livres, ou seja, se φ é uma sentença atômica , e é satisfeita por A , então se escreve

A ⊧ φ

Neste caso, pode-se também dizer que A é um modelo para φ, ou que φ é verdadeira em A . Se T é uma coleção de sentenças atômicas (uma teoria) satisfeita por A , escreve-se

A ⊧ T

Satisfatibilidade finita

Um problema relacionado à satisfatibilidade é o da satisfatibilidade finita , que é a questão de determinar se uma fórmula admite um modelo finito que a torna verdadeira. Para uma lógica que possui a propriedade de modelo finito , os problemas de satisfatibilidade e satisfatibilidade finita coincidem, pois uma fórmula dessa lógica possui um modelo se e somente se possui um modelo finito. Esta questão é importante no campo matemático da teoria dos modelos finitos .

A satisfatibilidade e a satisfatibilidade finitas não precisam coincidir em geral. Por exemplo, considere a fórmula lógica de primeira ordem obtida como a conjunção das seguintes sentenças, onde e são constantes : ${\ displaystyle a}$${\ displaystyle b}$

• ${\ displaystyle R (a_ {0}, a_ {0})}$
• ${\ displaystyle R (a_ {0}, a_ {1})}$
• ${\ displaystyle \ forall xy (R (x, y) \ rightarrow \ exists zR (y, z))}$
• ${\ displaystyle \ forall xyz (R (y, x) \ wedge R (z, x) \ rightarrow x = z))}$

A fórmula resultante possui o modelo infinito , mas pode-se demonstrar que não possui modelo finito (partindo do fato e seguindo a cadeia de átomos que deve existir pelo terceiro axioma, a finitude de um modelo exigiria a existência de um loop , o que violaria o quarto axioma, se ele volta para ou em um elemento diferente). ${\ displaystyle R (a_ {0}, a_ {0}), R (a_ {0}, a_ {1}), R (a_ {1}, a_ {2}), \ ldots}$${\ displaystyle R (a, b)}$${\ displaystyle R}$ ${\ displaystyle a_ {0}}$

A complexidade computacional de decidir satisfatibilidade para uma fórmula de entrada em uma dada lógica pode diferir daquela de decidir satisfazibilidade finita; na verdade, para algumas lógicas, apenas um deles é decidível .

Para a lógica de primeira ordem clássica , a satisfatibilidade finita é recursivamente enumerável (na classe RE ) e indecidível pelo teorema de Trakhtenbrot aplicado à negação da fórmula.

Restrições numéricas

Restrições numéricas freqüentemente aparecem no campo da otimização matemática , onde normalmente se deseja maximizar (ou minimizar) uma função objetivo sujeita a algumas restrições. No entanto, deixando de lado a função objetivo, a questão básica de simplesmente decidir se as restrições são satisfatórias pode ser desafiadora ou indecidível em alguns ambientes. A tabela a seguir resume os principais casos.

Restrições	sobre reais	sobre inteiros
Linear	PTIME (ver programação linear )	NP-completo (ver programação inteira )
Polinomial	decidível através, por exemplo, de decomposição algébrica cilíndrica	indecidível ( décimo problema de Hilbert )

Fonte da tabela: Bockmayr e Weispfenning .

Para restrições lineares, uma imagem mais completa é fornecida pela tabela a seguir.

Restrições sobre:	racionais	inteiros	números naturais
Equações lineares	PTIME	PTIME	NP-completo
Desigualdades lineares	PTIME	NP-completo	NP-completo

Fonte da tabela: Bockmayr e Weispfenning .

Veja também

• 2-satisfatibilidade
• Problema de satisfatibilidade booleana
• Satisfatibilidade do circuito
• 21 problemas NP-completos de Karp
• Validade
• Satisfação de restrição
• Satisficing

Notas

Referências

• Boolos e Jeffrey, 1974. Computabilidade e Lógica . Cambridge University Press.

Leitura adicional

• Daniel Kroening ; Ofer Strichman (2008). Procedimentos de decisão: um ponto de vista algorítmico . Springer Science & Business Media. ISBN 978-3-540-74104-6.
• A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009). Manual de Satisfabilidade . IOS Press. ISBN 978-1-60750-376-7.