Resolução SMT

Visão geral

A resolução de Satisfatibilidade Módulo Teorias (Satisfiability Modulo Theories, SMT) é o problema de decidir se uma fórmula lógica é satisfatível com respeito a uma ou mais teorias de fundo (background theories), tais como:

  • Aritmética linear (linear arithmetic) sobre inteiros ou reais (por exemplo, (x + y \le 10))
  • Vetores de bits (bit-vectors) (inteiros de máquina de largura fixa com operações bit a bit)
  • Arranjos (arrays) (memórias de leitura/escrita com select/store)
  • Funções não interpretadas (uninterpreted functions) (funções abstratas sem significado embutido, restringidas apenas por igualdade)

O SMT pode ser visto como uma extensão poderosa da resolução booleana de SAT (Boolean SAT solving): em vez de raciocinar apenas sobre variáveis true/false, solucionadores SMT raciocinam sobre objetos estruturados e restrições específicas de domínio, ainda explorando a velocidade da tecnologia moderna de SAT. Se SAT pergunta “existe uma atribuição para Booleanos que torne esta fórmula em forma normal conjuntiva (CNF) verdadeira?”, SMT pergunta “existe uma atribuição para Booleanos e variáveis de teoria (ints, reals, vetores de bits, arranjos, …) que torne esta fórmula verdadeira sob a semântica da teoria?”

A resolução SMT é fundamental em pipelines modernos de verificação e síntese, e está profundamente conectada a Resolução de SAT (SAT Solving), Solucionadores SAT (SAT Solvers) e métodos de verificação automatizada como Verificação de Modelos (Model Checking).

Fórmulas e teorias em SMT (o que “módulo teorias” significa)

Um problema SMT é tipicamente uma fórmula de lógica de primeira ordem (first-order logic) sem quantificadores (quantifier-free), construída a partir de:

  • Conectivos booleanos: and, or, not, =>, ite (if-then-else)
  • Igualdade e predicados de uma teoria (por exemplo, =, <=, ops bit a bit)
  • Termos de teoria (por exemplo, expressões inteiras, leituras/escritas de arranjos)

Uma teoria fornece:

  1. Um domínio de valores (por exemplo, inteiros, reais, vetores de bits de largura 32)
  2. Interpretações para símbolos de função e predicados (por exemplo, +, <=, bvadd)
  3. Uma noção de satisfatibilidade consistente com essas interpretações

O SMT é atraente porque muitas teorias úteis têm procedimentos de decisão (decision procedures) eficientes (algoritmos que decidem satisfatibilidade para aquela teoria) e porque problemas reais misturam estrutura booleana com restrições de teoria.

Teorias de fundo comuns (e por que elas importam)

Solucionadores SMT suportam muitas teorias; as mais comuns na prática incluem:

Aritmética Linear Inteira (LIA) e Aritmética Linear Real (LRA)

Restrições como:

  • 2*x + 3*y <= 10
  • x - y = 7
  • x >= 0

Elas surgem em escalonamento, restrições de recursos, invariantes, funções de ranking e muitas codificações de verificação.

Vetores de bits (BV)

Vetores de bits modelam inteiros de máquina com largura fixa e aritmética com overflow:

  • bvadd, bvsub, bvand, bvor, shifts, extracts/concats
  • Corresponde exatamente à semântica de programas de baixo nível (C/LLVM/ISA) de forma mais fiel do que inteiros matemáticos

Uma técnica comum é a explosão de bits (bit-blasting): reduzir restrições de vetores de bits a SAT expandindo operações em circuitos booleanos.

Arranjos

Arranjos modelam estruturas do tipo memória com:

  • select(A, i) (leitura)
  • store(A, i, v) (escrita, retorna um novo arranjo)

Arranjos são centrais para modelar heaps, pilhas, mapas de memória e mapas funcionais.

Funções não interpretadas (EUF: Igualdade com Funções Não Interpretadas)

EUF é usada para abstração:

  • Você pode declarar f(x) sem definir o que f faz.
  • O solucionador apenas assume congruência (congruence): se a = b então f(a) = f(b).

Isso é útil para componentes “caixa-preta”, verificação modular e loops de abstração-refinamento.

Outras teorias que você encontrará

  • Tipos de dados (datatypes) (tipos de dados algébricos, listas, árvores)
  • Strings e expressões regulares (regular expressions) (análise de programas, validação de entrada)
  • Ponto flutuante (floating-point) (semântica IEEE-754; mais difícil do que reais/inteiros)
  • Aritmética não linear (nonlinear arithmetic) (frequentemente indecidível ou muito difícil; solucionadores usam heurísticas)

Nota prática: a escolha de teoria afeta fortemente o desempenho. Modelar comportamento com precisão de bits usando inteiros pode estar errado; modelar aritmética de alto nível com vetores de bits pode ser lento.

Arquitetura central de solucionadores SMT: DPLL(T) / CDCL(T)

A maioria dos solucionadores SMT modernos é construída combinando:

  • Um solucionador SAT (SAT solver) (geralmente CDCL: aprendizado de cláusulas guiado por conflito (Conflict-Driven Clause Learning))
  • Um ou mais solucionadores de teoria (theory solvers) (para aritmética, arranjos, vetores de bits, EUF, …)
  • Um protocolo de comunicação entre eles (propagação, conflitos, explicações)

Essa arquitetura é comumente chamada DPLL(T) (histórica) ou CDCL(T) (moderna).

Abstração booleana

O solucionador SMT primeiro identifica átomos de teoria—predicados que pertencem a alguma teoria, como:

  • (<= x 5)
  • (= (+ x y) 10)
  • (= (select A i) 0)

Em seguida, ele substitui cada átomo por uma variável booleana nova para formar um esqueleto booleano (Boolean skeleton).

Exemplo de restrições SMT:

  • (x \ge 0)
  • (x \le 1 \lor x \ge 10)

Abstração booleana:

  • Deixe p significar (x >= 0)
  • Deixe q significar (x <= 1)
  • Deixe r significar (x >= 10)

Então a estrutura booleana se torna: p ∧ (q ∨ r)

Um solucionador SAT pode explorar atribuições como p=true, q=true e perguntar ao solucionador de teoria: “(x >= 0) ∧ (x <= 1) é consistente na teoria?” Se sim, continuar; se não, aprender uma cláusula que proíba essa combinação.

Laço CDCL(T) (alto nível)

Uma visão simplificada do laço principal:

  1. SAT decide atribuições booleanas (palpites) para átomos de teoria.
  2. O solucionador de teoria verifica consistência dos átomos atualmente afirmados dentro de sua teoria.
  3. Se consistente, o solucionador de teoria pode fazer propagação de teoria (theory propagation) (implicar átomos adicionais).
  4. Se inconsistente, o solucionador de teoria retorna um conflito de teoria (theory conflict) (uma explicação).
  5. O solucionador SAT realiza análise de conflito (conflict analysis) e aprende uma cláusula (um lema), então faz backtrack.

Isso continua até:

  • Uma atribuição consistente satisfazer todas as restrições (SAT) e um modelo ser produzido, ou
  • O solucionador SAT provar que nenhuma atribuição funciona (UNSAT)

Propagação de teoria

Solucionadores de teoria podem inferir consequências sem “chutar”. Por exemplo, em aritmética linear:

  • A partir de x >= 5 e x <= 3, derivar um conflito imediatamente.
  • A partir de x = y e y = 2, propagar x = 2.

A propagação é valiosa porque poda o espaço de busca do SAT cedo, de modo semelhante à propagação unitária em SAT, mas usando raciocínio de teoria.

Conflitos de teoria e aprendizado de conflitos

Quando o solucionador de teoria encontra inconsistência, ele retorna uma explicação—um subconjunto de átomos afirmados que não pode ser verdadeiro ao mesmo tempo. O solucionador SAT transforma isso em uma cláusula aprendida.

Exemplo (LIA):

  • Afirmado: x >= 5 e x <= 3
  • Explicação do conflito: (x >= 5) ∧ (x <= 3) é impossível
  • Cláusula aprendida: ¬(x >= 5) ∨ ¬(x <= 3)

Essa é a parte “T” do CDCL(T): o aprendizado ciente de teoria impede o solucionador de repetir a mesma combinação inconsistente.

Combinação de múltiplas teorias

Problemas reais frequentemente misturam teorias (por exemplo, arranjos + vetores de bits + igualdade). A combinação pode ser feita via:

  • Cooperação no estilo Nelson–Oppen (requer certas condições, por exemplo, assinaturas disjuntas (disjoint signatures) e “infinitude estável” (stable infiniteness) para garantias clássicas)
  • Solucionadores fortemente integrados (tightly integrated solvers) (comuns na prática, especialmente com vetores de bits e arranjos)
  • Abordagens de lemas sob demanda (lemma-on-demand) para interações específicas entre teorias

Na prática, solucionadores dependem de uma mistura de frameworks de combinação de teorias e heurísticas de engenharia.

SMT-LIB na prática: padrões de modelagem e exemplos

A maioria dos solucionadores SMT suporta a linguagem padrão SMT-LIB. O fluxo de trabalho típico é:

  • Declarar sorts e símbolos
  • Afirmar restrições
  • Chamar (check-sat)
  • Opcionalmente obter um modelo com (get-model) ou inspecionar um núcleo de insatisfatibilidade (unsat core)

Exemplo 1: Viabilidade em aritmética linear (LIA/LRA)

(set-logic QF_LIA)

(declare-const x Int)
(declare-const y Int)

(assert (>= x 0))
(assert (>= y 0))
(assert (= (+ x (* 2 y)) 7))

(check-sat)
(get-model)

Isso pede inteiros não negativos x, y tais que x + 2y = 7. O solucionador produzirá algo como x=1, y=3 (ou outra solução válida).

Dica de modelagem: use Int vs Real intencionalmente; restrições sobre inteiros geralmente são mais difíceis do que sobre reais, mas capturam a integralidade exatamente.

Exemplo 2: Funções não interpretadas para abstração (EUF)

Suponha que você queira raciocinar sobre uma função f mas não queira se comprometer com uma implementação:

(set-logic QF_UF)

(declare-sort U 0)
(declare-fun f (U) U)
(declare-const a U)
(declare-const b U)

(assert (= a b))
(assert (not (= (f a) (f b))))

(check-sat)

Isso é UNSAT porque EUF impõe congruência: de a=b segue f(a)=f(b).

Esse padrão é central na verificação modular: represente computações complexas como funções não interpretadas e então adicione apenas as propriedades de que você precisa (às vezes refinadas iterativamente).

Exemplo 3: Vetores de bits e overflow

Vetores de bits modelam overflow. Aqui mostramos que somar 1 ao valor máximo de 8 bits estoura para 0:

(set-logic QF_BV)

(define-const x (_ BitVec 8) #xff) ; 255
(define-const y (_ BitVec 8) (bvadd x #x01))

(assert (not (= y #x00)))

(check-sat)

Isso é UNSAT porque, em aritmética de 8 bits, #xff + 1 = #x00.

Dica de modelagem: se você precisa de comportamento fiel ao da máquina, vetores de bits geralmente são a escolha certa. Usar inteiros não capturaria bugs de overflow.

Exemplo 4: Arranjos com `select`/`store`

Arranjos são mapas funcionais imutáveis; store retorna um arranjo modificado.

(set-logic QF_AUFLIA)

(declare-const A (Array Int Int))
(declare-const i Int)

(define-const A2 (Array Int Int) (store A i 42))

(assert (not (= (select A2 i) 42)))
(check-sat)

Isso é UNSAT: ler no índice i após armazenar 42 em i deve retornar 42.

Arranjos são muito usados em modelagem de memória, execução simbólica e verificação de hardware.

Exemplo 5: Resolução incremental (`push`/`pop`) e consultas “e se”

Resolução incremental é importante em loops de verificação nos quais você adiciona restrições gradualmente.

(set-logic QF_LRA)

(declare-const x Real)

(assert (>= x 0))
(push)
  (assert (<= x 1))
  (check-sat) ; SAT
(pop)

(push)
  (assert (<= x -1))
  (check-sat) ; UNSAT
(pop)

Isso evita resolver do zero a cada vez.

Padrões comuns em SMT-LIB (checklist prático)

  • Use let para compartilhar subtermos e reduzir duplicação (ajuda desempenho e legibilidade).
  • Prefira fragmentos sem quantificadores quando possível (lógicas QF_*). Quantificadores frequentemente acionam instanciação heurística.
  • Use ite para codificar definições por partes, mas tenha cuidado: uso pesado pode explodir a estrutura booleana.
  • Se você precisa depurar:
    • (get-model) para atribuições satisfatíveis
    • (get-unsat-core) (quando suportado e habilitado) para identificar suposições conflitantes
    • Use check-sat-assuming para isolar subconjuntos de restrições

Aplicações típicas

Verificação formal e busca de bugs

Solucionadores SMT são motores centrais por trás de muitas ferramentas de verificação:

  • Verificação de modelos limitada (bounded model checking) e verificação simbólica de modelos (frequentemente em combinação com Verificação de Modelos)
  • Execução simbólica (symbolic execution): condições de caminho viram consultas SMT
  • Verificação de equivalência (equivalence checking): provar que duas implementações produzem as mesmas saídas
  • Verificação de invariantes (invariant checking): provar que asserções valem para todas as execuções (às vezes exigindo quantificadores ou indução)

Vetores de bits e arranjos são particularmente importantes para verificação de software/hardware porque modelam computação de baixo nível e memória com precisão.

Síntese de programas e síntese baseada em restrições

Em síntese, você busca um programa (ou parâmetros) que satisfaça uma especificação.

  • Codifique incógnitas como variáveis (ou escolhas de sintaxe como Booleanos)
  • Adicione restrições que capturem a especificação
  • Peça ao solucionador uma atribuição satisfatível que corresponda a um artefato sintetizado

Ecossistemas relacionados incluem SyGuS (síntese guiada por sintaxe (Syntax-Guided Synthesis)), em que solucionadores SMT frequentemente servem como backends.

Planejamento, configuração e raciocínio baseado em restrições em IA

SMT pode expressar restrições estruturadas que aparecem em tarefas de IA simbólica:

  • Planejamento com recursos numéricos (restrições de aritmética linear)
  • Restrições de configuração e dependências (EUF + aritmética)
  • Diagnóstico e verificação de consistência em sistemas baseados em conhecimento

Isso se conecta naturalmente a abordagens de satisfação de restrições na IA clássica (este artigo fica sob Satisfação de Restrições por esse motivo).

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

SMT (e técnicas intimamente relacionadas como programação linear inteira mista (MILP)/programação linear (LP) e codificações especializadas SAT/BV) pode ser usado para analisar propriedades de Redes Neurais (Neural Networks), especialmente modelos menores ou por partes lineares (por exemplo, redes ReLU (ReLU networks)). Tarefas comuns incluem:

  • Verificar robustez dentro de uma região de perturbação de entrada
  • Encontrar exemplos adversariais (adversarial examples) (como contraexemplos satisfatíveis)
  • Provar restrições de segurança para componentes de ML embarcados

Na prática, muitas ferramentas de verificação de redes neurais usam ideias de resolução de restrições no estilo SMT, embora possam depender de solucionadores especializados para escala.

Ecossistema de solucionadores e capacidades práticas

Solucionadores SMT populares incluem Z3, cvc5, Yices, Boolector (forte em vetores de bits/arranjos) e MathSAT. Embora seus pontos fortes difiram, muitos suportam:

  • Resolução incremental (push/pop)
  • Geração de modelos (get-model)
  • Núcleos de insatisfatibilidade e suposições
  • Registro de provas (proof logging) (em algumas configurações)
  • Procedimentos de decisão especializados por teoria

Competições como a SMT-COMP impulsionam padronização e melhorias de desempenho.

Considerações de desempenho (o que importa em cargas reais)

O desempenho de SMT é frequentemente determinado menos por “teoria de big-O” e mais por modelagem e heurísticas. Considerações-chave:

  • Escolha a teoria certa
    • Use vetores de bits para aritmética de máquina; use inteiros/reais para restrições em nível matemático.
  • Mantenha sem quantificadores quando puder
    • Quantificadores podem tornar problemas indecidíveis ou altamente heurísticos.
  • Reduza estrutura booleana desnecessária
    • Grandes aninhamentos de or/ite criam complexidade na busca SAT.
  • Explore incrementalidade
    • Loops de verificação se beneficiam muito de push/pop e do reuso de lemas aprendidos.
  • Prefira codificações mais fortes
    • Por exemplo, usar teoria nativa de arranjos pode superar codificações manuais (ou vice-versa) dependendo do solucionador e do problema.
  • Use suposições e núcleos de insatisfatibilidade para depuração
    • Quebre grandes conjuntos de restrições em grupos nomeados para encontrar conflitos mínimos.

Limitações e armadilhas comuns

  • Indecidibilidade e incompletude
    • Muitas lógicas úteis tornam-se indecidíveis com quantificadores, aritmética não linear ou certas combinações. Solucionadores podem retornar unknown em casos difíceis.
  • Surpresas com ponto flutuante
    • Ponto flutuante IEEE-754 não é aritmética real; restrições podem se comportar de forma inesperada se modeladas como reais.
  • Lacunas de abstração
    • Funções não interpretadas são poderosas, mas podem esconder semântica essencial; você pode precisar de refinamento (adicionar axiomas/lemas) para evitar modelos espúrios.
  • Interpretação de modelo
    • Um modelo satisfatível prova que existe uma atribuição; ele pode explorar graus de liberdade que você não pretendia (por exemplo, funções ou arranjos não restringidos). Restrinja o que você quer dizer.

Relação com resolução de SAT e tópicos relacionados

SMT se apoia diretamente na tecnologia de SAT—especialmente CDCL e aprendizado de cláusulas—mas adiciona raciocínio de teoria, propagação de teoria e aprendizado de lemas de teoria. Se você já entende Resolução de SAT, SMT é o próximo passo: SAT lida com o “esqueleto” booleano, enquanto solucionadores de teoria lidam com significado específico do domínio.

Para um contexto mais amplo, veja:

Resumo

A resolução SMT estende a resolução de SAT ao adicionar teorias de fundo que capturam aritmética, memória, computação em nível de bits e comportamento funcional abstrato. A arquitetura dominante—CDCL(T)—combina um mecanismo SAT com solucionadores de teoria via propagação de teoria e aprendizado guiado por conflitos. Com o padrão SMT-LIB, solucionadores SMT são ferramentas práticas para codificar e resolver tarefas reais de verificação, síntese e raciocínio por restrições, desde que você escolha teorias apropriadas e modele com cuidado.