Satisfatibilidade Módulo Teorias (SMT)

Visão geral

Satisfatibilidade Módulo Teorias (Satisfiability Modulo Theories, SMT) é uma família de problemas de decisão e tecnologias de solucionadores (solvers) para determinar se uma fórmula lógica é satisfatível (satisfiable) — não apenas em lógica booleana (Boolean logic) pura (como em SAT), mas sob “teorias de fundo (background theories)” adicionais como:

Aritmética linear de inteiros (Linear Integer Arithmetic, LIA) (por exemplo, restrições sobre inteiros com +, ≤)
Aritmética linear de reais (Linear Real Arithmetic, LRA) (restrições sobre racionais/reais)
Vetores de bits (bit-vectors) (aritmética de máquina de largura fixa com overflow)
Arranjos (arrays) (modelos de memória de leitura/escrita)
Funções não interpretadas (uninterpreted functions) (funções abstratas com raciocínio por igualdade)
Strings, ponto flutuante, tipos de dados algébricos e mais (com diferentes graus de maturidade/decidibilidade)

SMT é importante porque muitos problemas relacionados à inteligência artificial (AI) e a sistemas naturalmente envolvem uma mistura de estrutura booleana (“se isto, então aquilo”) e restrições ricas (“x + y ≤ 10”, “esta soma de 32 bits estoura”, “ler memória após escrever retorna o valor escrito”). Solucionadores SMT combinam:

Busca no estilo SAT (SAT-style search) com aprendizado guiado por conflitos (conflict-driven learning) (como em Resolução de SAT moderna)
Solucionadores de teoria (theory solvers) especializados (por exemplo, simplex para aritmética linear, fechamento por congruência para igualdades)

Essa combinação torna SMT uma base prática para verificação formal (formal verification), verificação de modelos (model checking), planejamento (planning) e modelagem baseada em restrições (constraint-based modeling).

De SAT a SMT

SAT em uma frase

Em SAT, você pergunta se uma fórmula booleana (frequentemente em CNF) possui uma atribuição de valores true/false que a torna verdadeira. Solucionadores de SAT modernos usam Aprendizado de Cláusulas Guiado por Conflito (Conflict-Driven Clause Learning, CDCL) para buscar com eficiência.

O que SMT acrescenta

SMT generaliza SAT ao permitir átomos (atoms) que não são apenas variáveis booleanas, mas predicados de teoria (theory predicates). Por exemplo:

Átomo SAT: p
Átomo SMT aritmético: (x + y ≤ 10)
Átomo SMT de vetores de bits: (bvult (bvadd a b) a) (padrões do tipo overflow sem sinal)
Átomo SMT de arranjos: (select A i) = v

Uma fórmula SMT pode parecer com:

(x > 0) ∧ (y > 0) ∧ (x + y = 10)

A pergunta é: Existe uma atribuição para x, y (no domínio pretendido da teoria) que satisfaça a fórmula?

SMT é frequentemente discutido em termos de fragmentos QF_T: “fórmulas sem quantificadores (quantifier-free formulas) sobre a teoria T” (por exemplo, QF_LIA para aritmética linear de inteiros sem quantificadores).

Teorias de fundo comuns (e por que importam)

O poder de SMT vem de escolher uma teoria que corresponda ao seu domínio.

Funções não interpretadas (Uninterpreted Functions, UF) e igualdade com funções não interpretadas (Equality with Uninterpreted Functions, EUF)

O que modela: Funções abstratas e raciocínio por igualdade sem se comprometer com detalhes de implementação.
Uso típico: Otimizações de compiladores, checagem de equivalência, análise de programas.
Raciocínio central: Fechamento por congruência (congruence closure) (se a=b então f(a)=f(b)).

Ideia de exemplo: impor consistência

Se a = b então f(a) = f(b)

Aritmética linear de inteiros (Linear Integer Arithmetic, LIA) e aritmética linear de reais (Linear Real Arithmetic, LRA)

O que modela: Restrições lineares como 2x + 3y ≤ 7.
Uso típico: Escalonamento, restrições de planejamento, recursos limitados.
Resolução: Métodos tipo simplex (simplex-like methods) (LRA), branch-and-bound/cortes (branch-and-bound/cuts) (LIA).

Decidibilidade/complexidade (importante na prática):

A satisfatibilidade de QF_LRA é resolvível em tempo polinomial (via programação linear sobre racionais).
QF_LIA é NP-completo (a integralidade torna mais difícil).

Vetores de bits (bit-vectors, BV)

O que modela: Inteiros de máquina de largura fixa com wraparound, operações bit a bit (bitwise operations), deslocamentos.
Uso típico: Verificação de hardware, verificação de software de baixo nível, restrições criptográficas.
Característica-chave: Captura exatamente como CPUs se comportam, diferentemente de inteiros matemáticos.

BV costuma ser reduzido a SAT via explosão de bits (bit-blasting) (transformar operações de vetores de bits em circuitos booleanos), mas muitos solucionadores também usam raciocínio em nível de palavra (word-level reasoning) para evitar a expansão completa.

Arranjos (arrays)

O que modela: Memória de leitura/escrita, mapas, arranjos funcionais.
Uso típico: Verificação de programas (heaps, memória), execução simbólica.
Axiomas centrais: select(store(A, i, v), i) = v e i ≠ j ⇒ select(store(A, i, v), j) = select(A, j).

Strings e linguagens regulares

O que modela: Restrições sobre strings (concatenação, substring, pertencimento a regex).
Uso típico: Análise de validação de entrada, testes de segurança, restrições de regras de PLN (em formas limitadas).
Observação prática: Poderoso, mas pode ficar caro; solucionadores usam métodos baseados em autômatos e equações de palavras.

Ponto flutuante (floating-point, FP)

O que modela: Comportamento de arredondamento IEEE-754.
Uso típico: Verificação de software numérico.
Observação prática: Mais complexo do que reais; frequentemente reduzido a vetores de bits.

SMT-LIB: a linguagem padrão de entrada

A maioria das ferramentas SMT aceita SMT-LIB, uma sintaxe semelhante a Lisp que padroniza teorias e comandos. Um fluxo de trabalho típico:

Declarar variáveis e seus sorts (sorts; tipos)
Afirmar restrições
Perguntar check-sat
Opcionalmente solicitar um modelo (get-model)

Exemplo 1: Aritmética linear (LIA)

Encontre inteiros x, y tais que x + y = 10 e ambos sejam não negativos.

(set-logic QF_LIA)
(declare-const x Int)
(declare-const y Int)

(assert (>= x 0))
(assert (>= y 0))
(assert (= (+ x y) 10))

(check-sat)
(get-model)

Um solucionador pode retornar sat com um modelo como x = 10, y = 0 (ou qualquer outra divisão que some 10).

Exemplo 2: Vetores de bits (BV) e intuição de overflow

Se a e b são valores sem sinal de 8 bits, então a + b faz wrap módulo 256. O seguinte procura um caso em que ocorre wraparound (a soma é menor do que um dos operandos):

(set-logic QF_BV)
(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))

(assert (bvugt b (_ bv0 8)))
(assert (bvult (bvadd a b) a)) ; wrapped around (unsigned)

(check-sat)
(get-model)

Esse tipo de consulta é comum na busca de bugs de baixo nível e na validação de aritmética de hardware.

Exemplo 3: Arranjos como memória

Modele um arranjo A atualizado no índice 5 para o valor 42, e então leia de volta:

(set-logic QF_AUFLIA)
(declare-const A (Array Int Int))

(define-fun A2 () (Array Int Int)
  (store A 5 42))

(assert (= (select A2 5) 42))
(check-sat)

Isso é a espinha dorsal da modelagem de atualizações de memória na análise de programas.

Como solucionadores SMT funcionam: SAT + raciocínio de teoria

Abstração booleana (o “esqueleto SAT”)

Um solucionador SMT tipicamente começa tratando cada átomo de teoria como uma variável booleana:

Deixe p representar (x > 0)
Deixe q representar (x + y = 10)
Deixe r representar (y > 0)

Então o solucionador explora atribuições booleanas para p, q, r usando um motor SAT. Mas, diferentemente de SAT puro, uma atribuição booleana também precisa ser consistente com a teoria (theory-consistent). Por exemplo, atribuir tanto (x = 0) quanto (x > 0) como verdadeiros é inconsistente em aritmética.

DPLL(T) / CDCL(T): a arquitetura central

O paradigma padrão é DPLL(T) (variantes modernas são frequentemente descritas como CDCL(T)):

O motor SAT propõe uma atribuição parcial a literais de teoria.
O solucionador de teoria verifica se os literais de teoria atualmente verdadeiros são consistentes na teoria T.
Se consistente, continue; se inconsistente, o solucionador de teoria retorna uma explicação de conflito (conflict explanation) (um lema (lemma)).
O motor SAT aprende esse lema (como uma cláusula (clause)) e faz retrocesso não cronológico.

Principais recursos adicionais além de “SAT + checagens ocasionais”:

Propagação de teoria (theory propagation): o solucionador de teoria pode deduzir literais implicados adicionais.
- Exemplo: a partir de x = 3 ele pode propagar (x ≥ 0) como verdadeiro.
Lemas de teoria (theory lemmas): quando o solucionador de teoria detecta inconsistência, ele retorna uma cláusula que bloqueia não apenas a atribuição atual, mas toda uma família de atribuições que causariam a mesma contradição.

Aprendizado guiado por conflitos com conflitos de teoria

Em SAT, um conflito surge de restrições booleanas; em SMT, conflitos podem surgir dentro do solucionador de teoria.

Exemplo (informal):

SAT atribui (x ≥ 5) como verdadeiro e (x ≤ 3) como verdadeiro
O solucionador de teoria aritmética diz: impossível
Ele retorna o lema: ¬(x ≥ 5) ∨ ¬(x ≤ 3)
O motor SAT aprende essa cláusula e faz backjump (backjump)

Esta é uma das razões pelas quais SMT escala: evita redescobrir repetidamente a mesma inconsistência de teoria.

Combinando múltiplas teorias

Problemas reais frequentemente envolvem múltiplas teorias, como arranjos + aritmética + funções não interpretadas. Solucionadores combinam solucionadores de teoria usando métodos como:

Combinação de Nelson–Oppen (Nelson–Oppen combination) (abordagem clássica sob certas condições)
Compartilhamento de igualdade entre solucionadores (eles comunicam igualdades sobre termos compartilhados)

Na prática, muitos solucionadores SMT integram múltiplas teorias de forma estreita, em vez de como caixas-pretas completamente separadas.

Quantificadores (um caso difícil, mas importante)

Embora muitos usos industriais permaneçam em SMT sem quantificadores (quantifier-free), quantificadores (forall, exists) são importantes para especificações (por exemplo, “para todo índice, a propriedade do arranjo vale”). SMT com quantificadores é, em geral, mais difícil e pode ser indecidível dependendo das teorias.

Abordagens comuns incluem:

E-matching / instanciação baseada em gatilhos (trigger-based instantiation) (gerar instâncias de fórmulas quantificadas)
Instanciação de quantificadores baseada em modelo (Model-Based Quantifier Instantiation, MBQI) (usar modelos candidatos para guiar instanciações)

Quantificadores são poderosos, mas podem causar não terminação ou explosões de custo se usados de forma ingênua.

Usos típicos em IA e sistemas

Verificação e verificação de modelos

SMT é central na verificação moderna:

Verificação de Modelo Limitada (Bounded Model Checking): desenrolar um sistema de transição por k passos e perguntar ao SMT se um estado ruim é alcançável.
Checagem de propriedades: propriedades de segurança (“algo ruim nunca acontece”) e checagens limitadas de vivacidade.

Isso se conecta diretamente à Verificação de Modelos, onde SMT frequentemente serve como o procedimento de decisão (decision procedure) subjacente quando o modelo inclui aritmética, arranjos ou operações com precisão de bits.

Execução simbólica e busca de bugs

Em execução simbólica (symbolic execution), entradas do programa são variáveis simbólicas. À medida que a execução explora caminhos, ela acumula restrições de caminho (path constraints):

Condição de desvio if (x > 0) adiciona a restrição (x > 0) naquele caminho
Outro desvio adiciona x + y = 10, etc.

Um solucionador SMT verifica:

Este caminho é viável?
Se sim, produza entradas concretas (um modelo) que o acionem

Isso é amplamente usado em geração de testes e análise de segurança.

Planejamento e modelagem baseada em restrições

Muitos problemas de planejamento podem ser codificados como restrições sobre passos de tempo, recursos e ações:

Escolhas booleanas: qual ação ocorre no tempo t
Restrições aritméticas: limites de recursos, custos, janelas de tempo

SMT suporta restrições mistas discretas/contínuas de modo mais natural do que SAT sozinho, então é útil para algumas formas de Planejamento Automatizado e escalonamento.

De forma relacionada, SMT pode ser visto como um motor poderoso para modelagem baseada em restrições ao lado de Problemas de Satisfação de Restrições tradicionais, especialmente quando você precisa de teorias ricas e explicações.

Síntese de programas e laços de resolução de restrições

SMT é frequentemente usado dentro de pipelines de síntese, por exemplo, Síntese Indutiva Guiada por Contraexemplos (Counterexample-Guided Inductive Synthesis, CEGIS):

Propor programa/parâmetros candidatos
Usar SMT para checar correção
Se incorreto, SMT produz um contraexemplo
Refinar o candidato e repetir

Usos adjacentes a ML: robustez e verificação de modelos aprendidos

SMT e solucionadores relacionados são usados para verificar propriedades de redes neurais (especialmente redes lineares por partes, como modelos baseados em ReLU), por exemplo:

“Para todas as entradas dentro de uma bola-ε desta imagem, o rótulo previsto permanece o mesmo.”

Essa área se sobrepõe a métodos formais mais do que ao treinamento convencional, mas é cada vez mais relevante para IA crítica em segurança (veja Redes Neurais para contexto).

Dicas práticas de modelagem (o que faz SMT funcionar bem)

Escolha a teoria certa
- Use vetores de bits quando precisar de semântica exata de máquina.
- Use inteiros/reais quando quiser aritmética matemática sem overflow.
Prefira codificações sem quantificadores quando possível
- Quantificadores podem ser poderosos, mas imprevisíveis.
- Muitas vezes você pode substituir forall sobre um pequeno domínio finito por conjunções explícitas.
Evite aritmética não linear a menos que seja necessário
- Aritmética inteira não linear é especialmente difícil e frequentemente indecidível com recursos adicionais.
- Se você puder linearizar ou limitar o problema, faça isso.
Use resolução incremental Muitos solucionadores suportam push/pop para adicionar/remover restrições eficientemente — útil em planejamento, verificação interativa e busca.
Tenha atenção às interações entre teorias Arranjos + aritmética + quantificadores pode ser muito mais difícil do que qualquer teoria isoladamente. Boas codificações reduzem o emaranhamento entre teorias.

Ecossistema de solucionadores e ferramentas

Solucionadores SMT populares incluem:

Z3 (Microsoft Research)
cvc5 (sucessor do CVC4)
Yices
Boolector (forte em vetores de bits/arranjos)
MathSAT

A maioria oferece:

Frontends SMT-LIB
APIs (bindings em C/C++/Java/Python variam por solucionador)
Recursos como resolução incremental, núcleos de insatisfatibilidade (unsat cores), objetos de prova (proof objects) (dependente do solucionador)

Essas ferramentas são amplamente embutidas em frameworks de verificação, motores de execução simbólica e ferramentas de síntese.

Fundamentos teóricos e limites

SMT fica na interseção entre lógica, teoria da complexidade e engenharia de algoritmos.

Muitas teorias sem quantificadores são decidíveis (decidable) e possuem procedimentos especializados eficientes (EUF, LRA).
Alguns fragmentos são NP-completos (NP-complete) (por exemplo, QF_LIA, QF_BV), mas são bastante tratáveis na prática devido ao aprendizado no estilo CDCL e a boas heurísticas.
Adicionar recursos (quantificadores, aritmética não linear, certas combinações de teorias) pode levar à indecidibilidade (undecidability) ou a penhascos severos de desempenho.

Uma lição prática fundamental: SMT é extremamente poderoso, mas o desempenho é sensível à codificação (encoding-sensitive). Duas formulações logicamente equivalentes podem diferir drasticamente no tempo de execução do solucionador.

Relação com tópicos correlatos

Se você quer o núcleo booleano, veja Resolução de SAT e Solucionadores de SAT práticos.
Para fluxos de trabalho de verificação automatizada onde SMT frequentemente é o motor, veja Verificação de Modelos.
Para detalhes de implementação e engenharia de solucionadores além da visão conceitual aqui, veja Resolução de SMT e Solucionadores de Satisfatibilidade Módulo Teorias (SMT).

Resumo

SMT estende SAT ao permitir restrições sobre domínios ricos (aritmética, vetores de bits, arranjos, funções não interpretadas e mais). Solucionadores SMT modernos têm sucesso porque integram:

Busca e aprendizado booleanos no estilo CDCL
Solucionadores de teoria que conseguem detectar contradições e propagar implicações
Lemas de teoria que podam grandes regiões do espaço de busca

Isso torna SMT uma tecnologia central para verificação, planejamento e modelagem baseada em restrições, e uma ponte fundamental entre lógica simbólica e sistemas computacionais do mundo real.