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 $$ \begin{aligned} & ((0, 0), 0) \quad ((0, 1), 1) \quad ((0, 2), 2) \quad \ldots \cr & ((1, 0), 1) \quad ((1, 1), 2) \quad ((1, 2), 3) \quad \ldots \cr \cr & \qquad\cdots\qquad ((21, 21), 42) \end{aligned} $$

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 é $\ndF$. Já se o candidato for $c = 42$ a decisão é $\ndT$.

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 = \begin{cases} \ndT &\text{se}~\exists v \del{v \models p} \ \ndF &\text{caso contrário} \end{cases} $$

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 = \begin{cases} \ndT &\text{se}~\forall v \del{v \models p} \ \ndF &\text{caso contrário} \end{cases} $$

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 = \begin{cases} \ndT &\text{se}~\vdash p \ \ndF &\text{caso contrário} \end{cases} $$

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 \models 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 \models 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 é $\mathbf{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 $\models p$ se e só se $\vdash p$ (o teorema da validade e completude).
A satisfação é equivalente à validade, porque se não existe $v$ tal que $v \models p$ ($p$ é uma contradição) então para qualquer $v$, $v \models \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.

Keyboard shortcuts