Satisfação de Restrições

Visão geral

Satisfação de restrições (constraint satisfaction) é uma ideia central na I.A. Clássica / Simbólica (Classical / Symbolic AI): descrever um problema afirmando o que deve ser verdadeiro (restrições), em vez de como computar uma solução (um algoritmo). Um solucionador (solver) então busca atribuições (assignments) que satisfaçam todas as restrições.

Essa família inclui:

  • CSP (Problemas de Satisfação de Restrições; Constraint Satisfaction Problems): variáveis com domínios finitos; restrições limitam combinações de valores.
  • SAT (Satisfatibilidade Booleana; Boolean Satisfiability): um caso especial de CSP com variáveis booleanas e restrições em lógica proposicional (frequentemente CNF).
  • SMT (Satisfatibilidade Módulo Teorias; Satisfiability Modulo Theories): SAT mais teorias de base como aritmética, arrays, vetores de bits ou funções não interpretadas.

Restrições são amplamente usadas em IA para escalonamento, planejamento, configuração, verificação e, cada vez mais, como “guardrails” e componentes estruturados em sistemas híbridos neuro-simbólicos (hybrid neuro-symbolic systems).

Na taxonomia da I.A. Clássica / Simbólica, a satisfação de restrições complementa Representação de Conhecimento (como codificar fatos e relações), Planejamento (Simbólico) (como gerar sequências de ações) e até Sistemas Especialistas (onde o raciocínio baseado em regras pode ser visto como imposição de restrições).

Problemas de Satisfação de Restrições (CSPs)

Definição formal

Um CSP é tipicamente definido como uma tríplice:

  • Variáveis: (X = {X_1, \dots, X_n})
  • Domínios (domains): (D = {D_1, \dots, D_n}), onde cada (D_i) é um conjunto finito de valores possíveis para (X_i)
  • Restrições (constraints): (C = {C_1, \dots, C_m}), em que cada restrição limita combinações permitidas de valores para um subconjunto (escopo (scope)) de variáveis

Uma solução (solution) é uma atribuição completa (X_i = v_i) com (v_i \in D_i) que satisfaz todas as restrições.

Exemplos

Coloração de mapas (clássico)

As variáveis são regiões, o domínio são cores {vermelho, verde, azul}, e as restrições dizem que regiões adjacentes devem ter cores diferentes.

  • Variáveis: (X_{WA}, X_{NT}, X_{SA}, \dots)
  • Domínios: ({R,G,B})
  • Restrições: (X_{WA} \ne X_{NT}), (X_{WA} \ne X_{SA}), ...

Isso ilustra um CSP de coloração de grafos (graph coloring).

Sudoku

As variáveis são as células, os domínios são {1..9}, e as restrições garantem:

  • cada linha tem todos os valores diferentes
  • cada coluna tem todos os valores diferentes
  • cada subgrade 3×3 tem todos os valores diferentes

O Sudoku é notável porque os solucionadores se beneficiam de restrições globais (global constraints) como AllDifferent (ver abaixo).

Escalonamento

As variáveis podem representar tempos de início de tarefas, os domínios são janelas/slots de tempo, e as restrições representam:

  • precedência (A antes de B)
  • capacidade (no máximo k tarefas em uma máquina ao mesmo tempo)
  • janelas de tempo (a tarefa deve ocorrer dentro de [t1, t2])

O escalonamento frequentemente vai além de um CSP “puro” para programação por restrições (constraint programming) (CP), com restrições mais ricas e propagação especializada.

Grafos de restrições e estrutura

Uma forma útil de raciocinar sobre a dificuldade de um CSP é a estrutura (structure):

  • Construa um grafo de restrições (constraint graph): nós = variáveis; arestas conectam variáveis que compartilham uma restrição.
  • Grafos em forma de árvore podem ser resolvidos com mais eficiência do que grafos densos.
  • Medidas como largura de árvore (treewidth) predizem tratabilidade: menor largura de árvore frequentemente significa resolução mais rápida.

Essa visão estrutural explica por que alguns CSPs grandes são resolvidos rapidamente (estrutura esparsa) enquanto alguns pequenos são difíceis (restrições densas e emaranhadas).

Resolvendo CSPs: busca + propagação

A maioria dos solucionadores de CSP práticos combina:

  1. Busca (search) (tipicamente com retrocesso) para explorar atribuições
  2. Propagação (propagation) para eliminar valores impossíveis cedo

Uma abordagem ingênua atribui variáveis uma a uma; quando uma restrição é violada, faz retrocesso.

Melhoria-chave: não apenas detectar violações — prever violações eliminando valores dos domínios.

Consistência e propagação

Noções de consistência definem o quão agressivamente eliminar valores:

  • Consistência de nó (node consistency): remove valores que violam restrições unárias.
  • Consistência de arco (arc consistency, AC): para cada valor de (X), existe um valor compatível em um vizinho (Y) sob cada restrição binária. AC-3 é um algoritmo clássico.
  • Consistência de caminho (path consistency): estende para triplas (mais custoso).

A propagação pode reduzir drasticamente a busca, às vezes resolvendo problemas com pouco ou nenhum retrocesso.

Heurísticas que importam na prática

Boas heurísticas frequentemente dominam o desempenho:

  • MRV (Minimum Remaining Values): escolher a variável com o menor domínio restante (falhar rápido).
  • Heurística de grau (Degree heuristic): desempatar escolhendo a variável envolvida no maior número de restrições.
  • LCV (Least Constraining Value): tentar valores que eliminam o menor número de opções para vizinhos.
  • Reinícios e aleatorização (restart and randomization): comuns em instâncias grandes.

Essas heurísticas conectam a resolução por restrições à ideia mais ampla de busca informada (informed search) em IA simbólica (também central em Planejamento (Simbólico)).

Restrições globais

Uma restrição global (global constraint) captura um padrão comum e vem com algoritmos fortes de propagação. Exemplos:

  • AllDifferent(x1, ..., xn) para permutações (Sudoku, atribuição)
  • Cumulative(tasks, capacity) para escalonamento de recursos
  • Element(index, array, value) para consultas em tabela
  • Circuit / NoSubtour para estrutura do tipo roteamento

Restrições globais são uma razão-chave pela qual solucionadores de CP se destacam em escalonamento e alocação de turnos, em comparação com codificações ingênuas.

De CSP para SAT

SAT em poucas palavras

SAT pergunta se uma fórmula de lógica proposicional é satisfazível. Na prática, as fórmulas frequentemente estão em Forma Normal Conjuntiva (Conjunctive Normal Form, CNF):

  • CNF é um AND de cláusulas
  • cada cláusula é um OR de literais
  • literal = variável ou sua negação

Exemplo de CNF:

[ (x \lor y \lor \lnot z) \land (\lnot x \lor z) ]

SAT é NP-completo (NP-complete), mas solucionadores SAT modernos lidam com instâncias enormes usando técnicas sofisticadas.

Codificando CSPs como SAT

Muitos CSPs de domínio finito podem ser codificados em SAT:

  • Para cada variável de CSP (X) com domínio ({v_1, \dots, v_k}), crie variáveis booleanas (x_{v_1}, \dots, x_{v_k}) significando “(X=v_i)”.
  • Adicione restrições de “exatamente um”:
    • pelo menos um valor: ((x_{v_1} \lor \dots \lor x_{v_k}))
    • no máximo um valor: ((\lnot x_{v_i} \lor \lnot x_{v_j})) para (i \ne j)
  • Codifique restrições entre variáveis como cláusulas (às vezes usando variáveis auxiliares).

Isso é conceitualmente simples, mas pode criar muitas cláusulas; o desempenho depende fortemente da qualidade da codificação.

Como funcionam solucionadores SAT modernos (DPLL/CDCL)

Solucionadores SAT modernos se baseiam em:

  • DPLL: busca com retrocesso com propagação unitária
  • CDCL (Aprendizado de Cláusulas Orientado por Conflitos; Conflict-Driven Clause Learning): quando ocorre um conflito, analisá-lo para aprender uma nova cláusula que evita repetir o mesmo erro
  • Propagação unitária (unit propagation): se uma cláusula se torna unitária (apenas um literal pode satisfazê-la), esse literal deve ser verdadeiro
  • Literais observados (watched literals), ramificação VSIDS (VSIDS branching), reinícios (restarts): inovações de engenharia que tornam solucionadores rápidos

Um insight central: o aprendizado (learning) transforma retrocesso bruto em algo mais próximo de construir uma prova de não satisfazibilidade quando não existe solução.

SMT: SAT + teorias

Por que SMT?

SAT é limitado à lógica puramente booleana. Muitos problemas de IA e de sistemas naturalmente envolvem:

  • inteiros e reais (tempo, custos)
  • vetores de bits (computação de baixo nível)
  • arrays (modelos de memória)
  • funções não interpretadas (funções simbólicas abstratas)

SMT estende SAT ao permitir essas expressões mais ricas, mantendo a eficiência no estilo SAT.

A arquitetura de SMT (DPLL(T))

Uma abordagem comum é DPLL(T):

  • Um solucionador SAT propõe uma atribuição booleana sobre a estrutura booleana da fórmula.
  • Um solucionador de teoria (theory solver) (para a teoria (T), por exemplo, aritmética linear) verifica se as restrições da teoria correspondentes são satisfazíveis em conjunto.
  • Se não forem, o solucionador de teoria retorna um lema de conflito (conflict lemma) (uma restrição aprendida) para refinar a busca SAT.

Essa combinação é poderosa: SAT lida com combinatória; solucionadores de teoria lidam com matemática.

Exemplo SMT-LIB (estilo Z3)

Aqui está um exemplo mínimo de SMT: encontrar inteiros (x, y) que satisfaçam restrições lineares.

(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 é mais difícil de expressar de forma eficiente em SAT puro sem um cuidadoso desdobramento em bits (bit-blasting) ou codificações.

Variantes de otimização: MaxSAT e OMT

Muitos problemas de IA não são apenas “existe uma solução?”, mas “qual é a melhor solução?”

  • MaxSAT: maximizar cláusulas satisfeitas (ou minimizar as violadas), frequentemente com pesos.
  • OMT (Otimização Módulo Teorias; Optimization Modulo Theories): otimizar um objetivo (por exemplo, minimizar custo) sujeito a restrições SMT.

Isso conecta restrições à tomada de decisão e ao planejamento sob objetivos.

Onde restrições ajudam em sistemas de IA

Resolução por restrições não é “IA antiga”; ela permanece um alicerce prático para muitos sistemas em produção e complementa cada vez mais o aprendizado de máquina (machine learning).

1) Planejamento e raciocínio sobre tarefas

O planejamento simbólico frequentemente se reduz a busca no espaço de estados; restrições podem fortalecer o planejamento ao:

  • eliminar cedo sequências de ações inviáveis
  • impor limites de recursos e relações temporais
  • codificar alcançabilidade ou invariantes

Muitos planejadores traduzem problemas para SAT/SMT (“planejamento como satisfatibilidade”), especialmente para planejamento com horizonte limitado:

  • escolher ações para cada passo de tempo
  • adicionar restrições que codificam a dinâmica de transição
  • resolver com SAT/SMT

Essa perspectiva se encaixa naturalmente ao lado de Planejamento (Simbólico).

2) Escalonamento, alocação de turnos e alocação de recursos

Esta é uma aplicação emblemática da programação por restrições:

  • escalas de pessoal (regras trabalhistas, restrições de cobertura)
  • escalonamento job-shop (job-shop scheduling) na manufatura
  • alocação de recursos em nuvem
  • gradeamento/horários escolares

Restrições frequentemente são a forma mais sustentável de codificar regras de negócio: você adiciona ou modifica restrições em vez de reescrever algoritmos.

Exemplo prático (Python OR-Tools CP-SAT, simplificado):

from ortools.sat.python import cp_model

model = cp_model.CpModel()

# Start times for two tasks
s1 = model.new_int_var(0, 10, "s1")
s2 = model.new_int_var(0, 10, "s2")

dur1, dur2 = 3, 4

# Non-overlap on a single machine: either task1 before task2 or vice versa
b = model.new_bool_var("t1_before_t2")
model.add(s1 + dur1 <= s2).only_enforce_if(b)
model.add(s2 + dur2 <= s1).only_enforce_if(b.Not())

# Objective: minimize makespan
makespan = model.new_int_var(0, 20, "makespan")
model.add_max_equality(makespan, [s1 + dur1, s2 + dur2])
model.minimize(makespan)

solver = cp_model.CpSolver()
print(solver.solve(model), solver.value(makespan))

Mesmo este pequeno exemplo mostra um padrão típico: variáveis de decisão + restrições + objetivo.

3) Configuração e design de produto (design combinatório)

Restrições são naturais para configuração:

  • regras de compatibilidade (se A então não B)
  • restrições de capacidade (orçamento de energia, limites de memória)
  • modelos de funcionalidades (comuns em linhas de produto de software)

Frequentemente isso é resolvido via SAT/SMT porque muitas regras são essencialmente booleanas.

4) Verificação, segurança e conformidade em sistemas habilitados por IA

SMT é amplamente usado em métodos formais (formal methods):

  • verificar lógica de controle e propriedades de segurança
  • checar invariantes em lógica de decisão
  • verificar propriedades de redes neurais (ferramentas de pesquisa/industriais frequentemente usam abstrações SMT/MILP)

Em pipelines de IA, restrições atuam como garantias (guarantees):

  • saídas devem respeitar limites rígidos
  • decisões devem satisfazer regras de política
  • transformações de dados devem satisfazer restrições de esquema

Isso é especialmente relevante quando saídas de ML alimentam sistemas com requisitos estritos (médico, automotivo, finanças).

5) Representação de conhecimento e raciocínio baseado em regras

Restrições se sobrepõem a sistemas baseados em regras:

  • uma regra como “se o paciente tem alergia X, não prescrever o medicamento Y” é uma restrição sobre ações permitidas.
  • muitas verificações de consistência lógica em Representação de Conhecimento podem ser formuladas como satisfatibilidade.

Formulações baseadas em restrições também podem apoiar explicações (explanations): “esta atribuição é impossível porque as restrições A e B entram em conflito.”

6) ML híbrido + restrições (neuro-simbólico e inferência com restrições)

O aprendizado de máquina frequentemente produz escores ou probabilidades, mas a saída final pode precisar satisfazer uma estrutura:

  • Predição estruturada (structured prediction): impor sequências válidas de rótulos (por exemplo, marcação BIO em PLN).
  • Decodificação com restrições (constrained decoding): durante a geração, restringir saídas a uma gramática, esquema ou conjunto permitido.
  • Restrições de equidade e de política (fairness and policy constraints): impor restrições sobre alocações ou recomendações.
  • Regularização posterior (posterior regularization) / aprendizado orientado por restrições (constraint-driven learning): incentivar modelos a satisfazer restrições lógicas suaves durante o treinamento.

Nesses cenários, restrições podem ser:

  • Restrições rígidas (hard constraints): devem sempre valer (por exemplo, a saída deve ser um JSON válido com um esquema específico).
  • Restrições suaves (soft constraints): violações incorrem em penalidade (otimizar trade-offs via MaxSAT/OMT, ou via penalidades diferenciáveis).

Restrições tornam-se uma ponte entre a flexibilidade estatística do ML e a confiabilidade de regras simbólicas.

Modelagem: como escrever restrições que resolvem bem

O desempenho de um solucionador depende tanto do modelo (model) quanto do algoritmo.

Boas práticas

  • Prefira restrições globais quando disponíveis (AllDifferent, cumulative, circuit).
  • Use domínios apertados (tight domains) (intervalos pequenos) para ajudar a propagação.
  • Faça quebra de simetria (symmetry breaking) (por exemplo, fixar uma variável arbitrária) para reduzir busca redundante.
  • Escolha o nível certo de abstração:
    • SAT se destaca em estrutura puramente booleana.
    • CP se destaca em restrições combinatórias ricas e primitivas de escalonamento.
    • SMT se destaca quando aritmética/arrays/funções importam.

Armadilhas comuns

  • Codificações fracas demais (muitas variáveis auxiliares sem força de propagação).
  • Problemas mistos contínuos/discretos sem a classe correta de solucionador (pode requerer MILP/CP-SAT/SMT ou decomposição).
  • Tratar preferências suaves como restrições rígidas (levando a “UNSAT” quando você na verdade queria o “melhor possível”).

Complexidade e limites

Satisfação de restrições é poderosa, mas não é mágica:

  • CSP geral e SAT são NP-completos; tempo exponencial no pior caso é inevitável sob suposições padrão de complexidade.
  • O desempenho real depende de:
    • estrutura da instância (esparsidade, modularidade)
    • rigidez das restrições (constraint tightness)
    • força de propagação
    • cláusulas aprendidas (SAT/SMT) e heurísticas de busca

Quando restrições se tornam extremamente grandes e ruidosas — comum em tarefas pesadas de percepção — resolução puramente por restrições geralmente não é a ferramenta certa. É aí que ML brilha, frequentemente combinado com restrições na camada de decisão.

Ferramentas e ecossistemas (orientação prática)

Famílias comuns de solucionadores:

  • CP / CP-SAT: Google OR-Tools, Gecode, Choco, MiniZinc (linguagem de modelagem + backends)
  • SAT: MiniSAT/Glucose/Cadical/Kissat (o panorama de solucionadores evolui rapidamente)
  • SMT: Z3, cvc5, Yices (com formatos padrão SMT-LIB)

Um fluxo de trabalho típico:

  1. Modelar variáveis, domínios, restrições e objetivo.
  2. Escolher uma classe de solucionador (CP vs SAT vs SMT) que corresponda aos tipos de restrição.
  3. Começar com um modelo correto; depois iterar por desempenho (restrições globais, quebra de simetria, codificações melhores).
  4. Adicionar instrumentação (instrumentation): limites de tempo, logs do solucionador, análise de inviabilidade.

Resumo

Satisfação de restrições fornece uma lente unificadora para muitos métodos de IA simbólica:

  • CSPs modelam decisões discretas com restrições e são resolvidos via busca + propagação.
  • SAT escala raciocínio booleano usando CDCL, aprendizado de cláusulas e heurísticas poderosas.
  • SMT estende SAT com aritmética e outras teorias, permitindo raciocínio expressivo com forte automação.

Em sistemas modernos de IA, restrições são mais valiosas onde validade, segurança, estrutura e regras de negócio importam — frequentemente complementando ML, em vez de competir com ele.