Problemas e Algoritmos

Que problemas podem ser resolvidos algoritmicamente?

Muitos problemas numéricos, por exemplo.
Ordenação, Criptografia, Programação Linear, etc

E sobre problemas na lógica?

Problemas e Instâncias

É necessário começar por definir (semi-formalmente) o que é um problema e uma instância e a diferença entre resolver e decidir

Definição (Problema, Instância, Resolver, Decidir)

Um problema é um conjunto de pares (instância, resposta).

Resolver consiste em calcular a resposta que corresponde a uma instância.
Decidir consiste em verificar se um candidato é, ou não, a resposta de uma instância.

Exemplo. Problema da soma

O problema da soma consiste no conjunto de pares $((a, b), c)$ em que $c = a + b$ . Algumas dos pares deste problema são $((0, 0), 0) ((0, 1), 1) ((0, 2), 2) \dots ((1, 0), 1) ((1, 1), 2) ((1, 2), 3) \dots ((21, 21), 42)$

A resolução da soma tem como "entrada" uma instância $(a, b)$ e consiste em calcular um $c$ de forma que $a + b = c$ . Por exemplo, dada a instância $(a, b) = (20, 22)$ a resolução é $c = 42$ .

A decisão da soma tem como "entradas" uma instância $(a, b)$ e um candidado $c$ e consiste em verificar se $c = a + b$ , isto é, se $c$ é uma resposta da instância $(a, b)$ . Por exemplo, dada a instância $(a, b) = (27, 15)$ e o candidato $c = 40$ a decisão é $f$ . Já se o candidato for $c = 42$ a decisão é $v$ .

Problemas Computacionais da Lógica Proposicional

Definição (SAT)

O problema da satisfação (SAT) consiste no conjunto de pares $(p, b)$ em que $p$ é uma proposição e $b$ um valor booleano tal que $b = {v f se \exists v (v ⊨ p) caso contr \overset{a}{ˊ} rio$

Isto é, Dada uma proposição, determinar se essa proposição tem um modelo.

Nos Tipos de Proposições, uma proposição que tenha algum modelo é compatível ou satisfazível.

Definição (Validade)

O problema da validade consiste no conjunto de pares $(p, b)$ em que $p$ é uma proposição e $b$ um valor booleano tal que $b = {v f se \forall v (v ⊨ p) caso contr \overset{a}{ˊ} rio$

Isto é, Dada uma proposição, determinar se essa proposição é válida.

Nos Tipos de Proposições, para uma proposição válida (ou tautologia) todas as valorações são modelos.

Definição (Provabilidade)

O problema da provabilidade consiste no conjunto de pares $(p, b)$ em que $p$ é uma proposição e $b$ um valor booleano tal que $b = {v f se ⊢ p caso contr \overset{a}{ˊ} rio$

Isto é, Dada uma proposição, determinar se essa proposição é um teorema.

Um teorema é uma proposição que tem uma prova (sem hipóteses).

O Problema da Satisfação (SAT)

Existe uma valoração $v$ tal que $v ⊨ p$ ?

É fácil fazer um algoritmo para resolver a este problema. Por exemplo, em Rust:

#![allow(unused)]
fn main() {
fn sat(p: Proposition) -> bool  {
  let vs = valorations(p);  // gerar todas as valorações de p
  for vi in vs  {           // para cada valoração vi...
    if vi(p) {              // testar se vi é modelo de p
      return true;          // nesse caso, devolver "true"
    }
  }
  return false;             // se não foi encontrado um modelo, devolver "false"
}
}

O problema é que vs tem $2^{n}$ elementos se $p$ tiver $n$ átomos. Se $p$ for satisfazível o algoritmo termina antes de testar todas as valorações. Mas, se $p$ não for satisfazível então este algoritmo vão ser testadas todas as $2^{n}$ valorações obtidas.

Este algoritmo não é eficiente porque consome demasiado tempo (a fazer as $2^{n}$ verificações no pior caso) e espaço (a memória para guardar todas as valorações).

Supondo que um computador que faz $1000000$ de verificações vi(p) por segundo:

Se $p$ tiver $100$ átomos existem $2^{100} = 1267650600228229401496703205376$ valorações, e demora $\approx 1267650600228229401496703$ segundos, isto é $\approx 40196936841331$ milhões de milénios a verificar $p$ , no pior caso.
Em comparação, o universo tem uma idade estimada de 13787 milhões de milénios; seriam necessárias $\approx 3000$ milhões de vidas do universo para resolver este problema para uma única proposição.
Mesmo melhorando milhões de vezes a velocidade dos computadores este algoritmo não é utilizável na prática — e $100$ átomos é um exemplo muito modesto.

Embora seja tecnicamente possível converter a função valorations num iterador, resolvendo o problema do espaço, ainda assim continua a fazer as $2^{n}$ verificações — o problema do tempo persiste!.

Existe um algoritmo eficiente para resolver SAT? Ninguém sabe!

Quem resolver SAT eficientemente tem Fama, Fortuna & Glória Instantâneas, Universais & Eternas &tc.

O Interesse do Problema da Satisfação

Uma única proposição $p$ pode descrever um sistema complexo:

Um automóvel.
Um foguetão.
Uma central nuclear.
A economia de um país.
O clima de um planeta.
Um ser vivo.
A ecologia de uma região.
O funcionamento de um programa.
...

Um modelo $v ⊨ p$ descreve as condições para atingir um objetivo e/ou as consequências de uma ação.

Resolver SAT eficientemente (por exemplo, em tempo polinomial) iria permitir uma revolução em todos os setores da atividade humana: política, gestão, engenharia, etc.

Os Problemas do Problema da Satisfação

Embora sejam conhecidos algoritmos que resolvem rapidamente problemas SAT com dezenas de milhar de variáveis, a complexidade computacional é desconhecida no caso geral.
SAT é $NP$ -completo. Isto significa que pode ser decidido em tempo polinomial e ser usado para resolver vários problemas de otimização, desenho de circuitos, inteligência artificial, etc.
A linguagem da lógica proposicional não descrimina objetos de um domínio nem como estes se relacionam — portanto SAT sofre também desta limitação.

Os Outros Problemas

A validade é equivalente à provabilidade, porque $⊨ p$ se e só se $⊢ p$ (o teorema da validade e completude).
A satisfação é equivalente à validade, porque se não existe $v$ tal que $v ⊨ p$ ( $p$ é uma contradição) então para qualquer $v$ , $v ⊨ \neg p$ ( $\neg p$ é válida).

Problemas Equivalentes. Intuitivamente dois problemas A e B são equivalentes se um algoritmo para resolver A pode ser eficientemente adaptado para resolver B e vice-versa.