Parte IV · Cap. 18 — Programação Lógica / Solvers
Simbólica · Raciocínio formal · Resolução / SAT-SMT. Resolve problemas declarados como fórmulas lógicas ou restrições — com correção garantida. Card:
../02-tipos-de-ia/01-simbolica.kmd.
🎨 Figura
F-IV.18.0— Da fórmula à solução. Brief: um conjunto de restrições lógicas entrando num solver que retorna SAT (com atribuição) ou UNSAT; árvore de backtracking estilizada.
1. Definição e história curta
Resolve satisfatibilidade e restrições por busca lógica completa. Linhagem: Prolog (1972), projeto Quinta Geração (Japão, 1982), e solvers SAT/SMT modernos (Z3) onipresentes em verificação.
2. Fundamentos
- Lógica matemática / teoria da prova — satisfatibilidade, resolução.
- Complexidade — SAT é o NP-completo canônico.
- Combinatória — busca em espaço de atribuições.
3. Algoritmos e arquiteturas
- Resolução / unificação — base do Prolog.
- DPLL / CDCL — núcleo dos solvers SAT modernos (conflict-driven).
- SMT — SAT + teorias (aritmética, arrays); ex.: Z3.
- ASP / CP — Answer Set Programming, constraint programming.
4. Insumos
- Hardware: CPU; alguns problemas explodem (NP).
- Dados: a formulação do problema (cláusulas/restrições).
- Estruturas de dados: cláusulas, implication graph, trail.
- Sistemas: Prolog, MiniSat, Z3, OR-Tools.
5. Ciclo de vida especializado
| Etapa | Especialização |
|---|---|
| 0 Problema | Problema formalizável em lógica/restrições |
| 1 Dados | Codificar o problema (cláusulas, teorias) |
| 2 EDA | Estrutura/dificuldade da instância |
| 3 Modelagem | Escolher SATSMTCP; codificação eficiente |
| 4 "Treino" | Não há — há formulação; solvers têm heurísticas |
| 5 Avaliação | Corretude (garantida), tempo até solução |
| 5.5 Homologação | Validar a codificação contra o problema real |
| 6 Produção | Resolver instâncias; timeouts/heurísticas |
| 7 Monitoramento | Instâncias difíceis, tempo |
| 8 Manutenção | Reformular conforme o domínio muda |
| 9 Governança | Confiabilidade da prova/verificação |
6. Capacidades, modos e modalidades
Dedutivo/verificação: verificação de hardware/software, escalonamento, configuração, prova; correção garantida quando termina.
7. Limites, riscos e ética
NP-dureza (pode não escalar); exige formalização exata; sem aprendizado. Ponto forte: garantias formais — daí o papel central no neuro-simbólico (cap. 32) e na IA confiável.
8. Estado da arte e exemplos
Z3 (SMT), CDCL SAT solvers, OR-Tools; verificação formal, síntese de programas; LLM + solver (o LLM formaliza, o solver garante) é tendência de raciocínio confiável.