Resolução de SAT

Visão geral

A satisfatibilidade booleana (Boolean satisfiability, SAT) é o problema de decidir se existe uma atribuição de valores de verdade a variáveis booleanas que faça uma fórmula booleana avaliar como verdadeira. Apesar de sua formulação simples, SAT é um pilar da satisfação de restrições (constraint satisfaction) e da I.A. simbólica (symbolic AI) porque:

É NP-completo (NP-complete) (Cook–Levin), então muitos problemas combinatórios difíceis podem ser reduzidos a ele.
Solucionadores de SAT modernos lidam rotineiramente com instâncias com milhões de variáveis/cláusulas usando técnicas sofisticadas de busca, propagação e aprendizado.
Muitas tarefas de IA—especialmente em Planejamento Automatizado, verificação e escalonamento—podem ser codificadas em SAT e resolvidas de forma eficiente.

Este artigo foca SAT em forma normal conjuntiva (conjunctive normal form, CNF) e as principais famílias de algoritmos usadas na prática, especialmente DPLL e CDCL.

Para detalhes de implementação e engenharia (estruturas de dados, arquiteturas de solucionadores, benchmarking), veja a página irmã Solucionadores de SAT.

Definição do problema

Variáveis, literais, cláusulas, fórmulas

Uma variável booleana (Boolean variable) é um símbolo como (x) que pode ser verdadeiro ou falso.
Um literal (literal) é uma variável (x) (literal positivo) ou sua negação (\neg x) (literal negativo).
Uma cláusula (clause) é uma disjunção (OR) de literais, por exemplo ((x \lor \neg y \lor z)).
Uma fórmula em CNF é uma conjunção (AND) de cláusulas, por exemplo: [ (x \lor y) \land (\neg x \lor z) \land (\neg y \lor \neg z) ]

Uma fórmula em CNF é satisfatível (satisfiable) se alguma atribuição a todas as variáveis torna toda cláusula verdadeira; caso contrário, ela é insatisfatível (unsatisfiable, UNSAT).

Por que CNF?

Solucionadores de SAT quase universalmente operam em CNF porque:

CNF funciona naturalmente com resolução (resolution), uma regra de inferência chave por trás do aprendizado de cláusulas.
Muitas técnicas de propagação (especialmente propagação unitária (unit propagation)) são eficientes em CNF.
Qualquer fórmula booleana pode ser convertida para CNF. Na prática, solucionadores usam uma transformação de Tseitin (Tseitin transformation) para preservar a satisfatibilidade enquanto mantêm o tamanho da CNF linear no tamanho do circuito/fórmula original (ao custo de introduzir variáveis auxiliares).

Exemplo de instância CNF

Considere: [ (x \lor y) \land (\neg x \lor y) \land (x \lor \neg y) ]

Tente (y = \text{true}). Então todas as cláusulas são verdadeiras independentemente de (x), logo a fórmula é satisfatível.

Formato DIMACS CNF (prático)

A maioria das ferramentas de SAT aceita DIMACS CNF:

c Example CNF: (x1 OR x2) AND (~x1 OR x2) AND (x1 OR ~x2)
p cnf 2 3
1 2 0
-1 2 0
1 -2 0

Variáveis são numeradas de 1..n
Um inteiro negativo denota negação
Cada cláusula termina com 0

Fundamentos teóricos (alto nível)

Complexidade e reduções

SAT é NP-completo, o que significa:

SAT está em NP: dada uma atribuição, conseguimos verificar a satisfação em tempo polinomial.
SAT é NP-difícil: todo problema em NP pode ser reduzido a SAT em tempo polinomial.

É por isso que SAT é um “backend universal” para muitos problemas combinatórios em IA e CC. Muitas tarefas em Problemas de Satisfação de Restrições podem ser mapeadas para SAT.

Sistemas de prova e resolução

Uma razão-chave para solucionadores de SAT conseguirem provar UNSAT é sua conexão com a resolução. A resolução afirma que, a partir de:

((A \lor x)) e ((B \lor \neg x))

podemos inferir:

((A \lor B))

Solucionadores CDCL (conflict-driven clause learning) modernos efetivamente constroem provas por resolução via cláusulas aprendidas. Isso não é apenas teórico: cláusulas aprendidas são o mecanismo pelo qual o solucionador memoriza conflitos e evita repetir os mesmos padrões de busca que falham.

Técnicas centrais de solucionadores: DPLL e CDCL

DPLL: o algoritmo clássico de SAT por retrocesso

O procedimento Davis–Putnam–Logemann–Loveland (DPLL) é o algoritmo completo clássico para SAT. Conceitualmente, ele é:

Propagar (propagate) atribuições forçadas (especialmente cláusulas unitárias).
Se uma cláusula se torna falsa → conflito (conflict) → retroceder.
Se todas as variáveis forem atribuídas e não houver conflitos → SAT.
Caso contrário, escolher uma variável de ramificação e recursar.

Um esboço mínimo de pseudocódigo:

DPLL(F, assignment):
  assignment := UnitPropagate(F, assignment)
  if conflict: return UNSAT
  if all variables assigned: return SAT

  x := ChooseBranchVariable(F, assignment)
  return DPLL(F, assignment ∪ {x=true}) OR
         DPLL(F, assignment ∪ {x=false})

DPLL já é poderoso, mas solucionadores modernos avançam com aprendizado de cláusulas guiado por conflito (conflict-driven clause learning, CDCL).

CDCL: DPLL + aprendizado + retrocesso não cronológico

CDCL é o paradigma dominante em resolução de SAT hoje. Ele aprimora DPLL com:

Propagação unitária (o principal motor de inferência)
Análise de conflito (conflict analysis) para explicar por que um conflito ocorreu
Aprendizado de cláusulas (clause learning) para evitar repetir o mesmo erro
Retrocesso não cronológico (non-chronological backtracking) (salto para trás) até o nível de decisão relevante
Reinícios (restarts) para escapar de partes ruins do espaço de busca
Heurísticas sofisticadas de ramificação (branching heuristics) (por exemplo, VSIDS)

Em alto nível, CDCL mantém:

Uma atribuição parcial dividida em níveis de decisão (decision levels)
Um grafo de implicação (implication graph) registrando por que variáveis foram implicadas
Um banco de dados de cláusulas originais + cláusulas aprendidas

Propagação unitária (UP): o “motor” do solucionador

O que é propagação unitária?

Uma cláusula unitária (unit clause) é uma cláusula com exatamente um literal não atribuído e todos os outros literais falsos sob a atribuição parcial atual.

Cláusula de exemplo: [ (\neg x \lor y) ] Se (x = \text{true}), então (\neg x) é falso, então para satisfazer a cláusula devemos ter (y = \text{true}). Assim, a cláusula se torna unitária e implica (y).

A propagação unitária repete isso até não existirem mais cláusulas unitárias (um ponto fixo).

Por que isso é tão importante?

A propagação unitária pode derivar muitas consequências forçadas a baixo custo.
A maior parte do tempo de execução em SAT é gasta fazendo propagação unitária de forma eficiente.
A propagação unitária também é a base para detectar conflitos cedo.

Literais vigiados (ideia de implementação)

Propagação unitária eficiente na prática usa dois literais vigiados (two-watched literals) por cláusula:

Cada cláusula “vigia” dois literais que atualmente não são falsos.
Quando um literal vigiado se torna falso, o solucionador tenta mover a vigilância para outro literal não-falso na cláusula.
Uma cláusula se torna unitária apenas quando não consegue encontrar um substituto para uma vigilância e a outra vigilância está não atribuída/verdadeira.

Isso torna a propagação próxima de linear no número de atribuições propagadas, em vez de varrer todas as cláusulas repetidamente.

Conflitos, aprendizado de cláusulas e backjumping

Conflitos

Um conflito ocorre quando alguma cláusula fica inteiramente falsa sob a atribuição atual, o que significa que o caminho atual na árvore de busca não pode levar a uma solução.

Exemplo: a cláusula ((x \lor y)) se torna falsa se (x=false) e (y=false).

Grafo de implicação (intuição)

Durante a propagação, cada literal implicado tem uma “cláusula de motivo” explicando por que ele teve de ser verdadeiro. CDCL usa esses motivos para construir um grafo de implicação:

Nós: literais atribuídos
Arestas direcionadas: “esta atribuição implicou aquela atribuição”
Um conflito corresponde a derivar a falsidade de uma cláusula—frequentemente representado como um nó especial de conflito.

Aprendizado de cláusulas (análise de conflito)

Quando ocorre um conflito, CDCL o analisa para produzir uma cláusula aprendida (learned clause) que:

É logicamente implicada pela fórmula existente
Bloqueia a combinação atual de decisões que falha
Frequentemente causa propagação futura mais cedo

Uma estratégia comum é o aprendizado First UIP (Unique Implication Point), que tende a produzir cláusulas aprendidas fortes na prática.

Retrocesso não cronológico (backjumping)

Em vez de desfazer apenas a última decisão (retrocesso cronológico), CDCL calcula o maior nível de decisão que ainda é relevante para a cláusula aprendida e salta diretamente de volta para esse nível. Isso pode podar partes enormes do espaço de busca.

Heurísticas de ramificação

Solucionadores de SAT dependem criticamente de heurísticas de decisão: qual variável atribuir em seguida e com qual polaridade.

VSIDS e suas variantes

A heurística clássica e ainda influente é VSIDS — Soma Decrescente Independente do Estado da Variável (Variable State Independent Decaying Sum):

Cada variável tem uma pontuação de atividade.
Variáveis que aparecem em conflitos recentes têm sua pontuação aumentada.
As pontuações decaem ao longo do tempo, focando o solucionador na parte “quente” atual da fórmula.

Solucionadores modernos também usam variantes como EVSIDS, LRB e estratégias híbridas, mas o princípio é o mesmo: focar decisões onde conflitos ocorrem.

Seleção de polaridade

Ao ramificar na variável (x), o solucionador precisa escolher (x=true) ou (x=false) primeiro. Heurísticas de polaridade incluem:

Salvamento de fase (phase saving): reutilizar o último valor que funcionou bem antes de um reinício
Preferir uma polaridade que satisfaça mais cláusulas (dependente do problema)

Reinícios: “esquecimento” estratégico do caminho de busca

Reinícios abandonam intencionalmente a atribuição parcial atual (mantendo as cláusulas aprendidas) e então começam novamente. Isso parece desperdício, mas funciona porque:

Cláusulas aprendidas acumulam conhecimento global.
Reinícios evitam ficar preso explorando uma região ruim da árvore de busca.

Cronogramas comuns de reinício incluem:

Geométrico (geometric) (reiniciar após 100, 200, 400, … conflitos)
Sequência de Luby (Luby sequence), que tem boas propriedades teóricas para distribuições de tempo de execução desconhecidas

Reinícios são uma das razões pelas quais solucionadores modernos de SAT se comportam mais como sistemas de aprendizagem (learning systems) do que como busca por retrocesso pura.

Gerenciamento do banco de cláusulas: aprender sem explodir

Aprender cláusulas demais pode desacelerar a propagação e consumir memória. Por isso, solucionadores deletam cláusulas aprendidas periodicamente, mantendo aquelas que provavelmente serão úteis.

Sinais comuns para retenção:

LBD baixo — distância de bloqueio de literais (Literal Block Distance, LBD): uma medida de quantos níveis de decisão aparecem na cláusula; valores menores frequentemente significam “mais global/útil”
Alta atividade ou uso recente na propagação

Isso cria um equilíbrio dinâmico: aprender agressivamente e depois podar.

Pré-processamento e inprocessamento

Antes (e durante) a busca principal, solucionadores frequentemente simplificam a fórmula:

Eliminação de literal puro (pure literal elimination) (menos comum em loops internos de CDCL, mas usada no pré-processamento)
Subsunção (subsumption): remover cláusulas que são superconjuntos de outras
Eliminação de variáveis (variable elimination) via resolução limitada (bounded resolution)
Eliminação de cláusula bloqueada (blocked clause elimination)
Detecção de equivalência (equivalence detection) (identificar (x \leftrightarrow y))

Solucionadores modernos também fazem inprocessamento (inprocessing): intercalar etapas de simplificação com busca e aprendizado.

Codificando problemas em SAT

SAT é tão útil porque muitos problemas podem ser codificados como CNF com uma separação clara:

Modelagem (modeling) (escolher variáveis e restrições)
Resolução (solving) (executar um solucionador genérico de SAT)

Padrões comuns de codificação

“Pelo menos um” e “no máximo um”

Suponha que precisamos que exatamente um de ({a,b,c}) seja verdadeiro.

Pelo menos um: [ (a \lor b \lor c) ]
No máximo um (pareado): [ (\neg a \lor \neg b) \land (\neg a \lor \neg c) \land (\neg b \lor \neg c) ]

O pareado é simples, mas é (O(n^2)). Para conjuntos grandes, use codificações mais eficientes (contadores sequenciais (sequential counters), redes de cardinalidade (cardinality networks)). Muitos sistemas práticos baseados em SAT dependem fortemente de codificações de cardinalidade (cardinality encodings) compactas.

Implicação e equivalência

(a \rightarrow b) vira ((\neg a \lor b))
(a \leftrightarrow b) vira ((\neg a \lor b) \land (a \lor \neg b))

Exemplo trabalhado: um microproblema de planejamento

SAT é amplamente usado em planejamento como satisfatibilidade (planning-as-satisfiability): representar uma tarefa de planejamento com um horizonte de tempo fixo (T) como uma instância SAT e então aumentar (T) até ficar satisfatível.

Considere um domínio de “interruptor de luz” de brinquedo:

Variável de estado: On(t) significa que a luz está ligada no passo de tempo (t)
Ação: Toggle(t) alterna a luz entre (t) e (t+1)
Objetivo: fazer a luz ficar ligada no tempo (T)
Estado inicial: desligada no tempo 0

Precisamos de variáveis booleanas:

(On_t) para (t=0..T)
(Toggle_t) para (t=0..T-1)

Restrições (informais):

Estado inicial: (\neg On_0)
Transição: se Toggle, então o próximo estado inverte; se não, ele permanece igual

A dinâmica de alternância pode ser codificada como um OU-exclusivo (XOR): [ On_{t+1} \leftrightarrow (On_t \oplus Toggle_t) ] XOR não é CNF diretamente, mas pode ser codificado com cláusulas. Uma codificação CNF para (z \leftrightarrow (x \oplus y)) é:

((\neg x \lor \neg y \lor \neg z))
((\neg x \lor y \lor z))
((x \lor \neg y \lor z))
((x \lor y \lor \neg z))

Então, para cada (t), defina (x=On_t), (y=Toggle_t), (z=On_{t+1}) e adicione essas quatro cláusulas.

Objetivo: (On_T)

Agora o solucionador de SAT responde:

UNSAT para (T=0) (não pode estar ligada imediatamente a partir de desligada)
SAT para (T=1) com Toggle(0)=true

Isso ilustra um fluxo de trabalho padrão em planejamento:

Fixar o horizonte (T)
Codificar dinâmica e restrições como CNF
Resolver SAT
Se UNSAT, aumentar (T)

Isso é intimamente relacionado a métodos clássicos de planejamento como Graphplan, mas o planejamento baseado em SAT se beneficia de solucionadores CDCL extremamente otimizados. Para um contexto mais amplo de planejamento, veja Planejamento Automatizado.

Além do planejamento: outros problemas de restrições

Codificações em SAT aparecem por toda a IA e a CC:

Escalonamento / criação de horários: variáveis booleanas para atribuir tarefas a tempos/recursos; restrições impõem capacidades e precedências.
Verificação de modelos (model checking) e verificação: verificação de modelos limitada (bounded model checking) codifica “existe um contraexemplo de tamanho (k)?” como SAT. Veja Verificação de Modelos.
Teste de hardware/software: gerar entradas que satisfaçam condições de caminho (execução simbólica (symbolic execution) frequentemente termina em restrições SAT/SMT).
Configuração e diagnóstico: restrições garantem seleções compatíveis de componentes.
Quebra-cabeças combinatórios (Sudoku, N-Queens): exemplos clássicos de codificações SAT como CSPs.

Para restrições envolvendo aritmética, arrays ou funções não interpretadas, praticantes frequentemente usam Resolução SMT (SAT módulo teorias (SAT modulo theories)), que se baseia na tecnologia de SAT.

Padrões práticos de uso de solucionadores

SAT incremental e suposições

Muitas aplicações resolvem uma sequência de instâncias SAT relacionadas (por exemplo, aumentar o horizonte de planejamento (T), aprofundamento iterativo, ou adicionar restrições). Solucionadores modernos suportam SAT incremental (incremental SAT):

Manter o estado do solucionador e as cláusulas aprendidas
Adicionar cláusulas ao longo do tempo
Opcionalmente usar suposições (assumptions) (literais temporários) para testar variantes sem adicionar restrições permanentemente

Isso é crítico para desempenho em fluxos de trabalho de planejamento e verificação.

Interpretando as saídas do solucionador

Solucionadores tipicamente retornam:

SAT com uma atribuição satisfatória (um modelo)
UNSAT possivelmente com um traço de prova (para verificação certificada)
UNKNOWN é incomum para SAT puro (é um problema de decisão), mas pode ocorrer se limites de recursos forem atingidos (timeouts/memória).

SAT no panorama mais amplo de satisfação de restrições

SAT é um ponto em um espectro:

Solucionadores de CSP (Constraint Satisfaction Problems, CSPs) (restrições de domínio finito) enfatizam propagação em domínios mais ricos.
Solucionadores de SAT se destacam com estrutura booleana e escala massiva.
Solucionadores de SMT (Satisfiability Modulo Theories) combinam SAT com solucionadores de teorias para restrições mais ricas.
Satisfatibilidade máxima (Maximum Satisfiability, MaxSAT) / MaxSAT ponderado (Weighted MaxSAT) otimizam o número (ou o peso) de cláusulas satisfeitas—útil para restrições suaves e raciocínio por preferências.

Em muitos sistemas de IA, uma decisão-chave de modelagem é se deve codificar diretamente em SAT, usar SMT, ou usar um CSP de nível mais alto e deixar que ele compile para baixo.

Resumo

A resolução de SAT transforma uma ampla gama de problemas discretos de IA e de restrições na pergunta: existe uma atribuição booleana que satisfaça uma fórmula em CNF? O sucesso prático de SAT se apoia em solucionadores CDCL, que combinam:

Propagação unitária (inferência rápida)
Análise de conflito + aprendizado de cláusulas (transformar falhas em conhecimento reutilizável)
Backjumping (podar busca irrelevante)
Heurísticas de ramificação como VSIDS (focar em regiões com muitos conflitos)
Reinícios (escapar de caminhos de busca improdutivos mantendo cláusulas aprendidas)

Ao codificar tarefas como planejamento, escalonamento e verificação em CNF, solucionadores de SAT servem como motores poderosos de uso geral para raciocínio simbólico dentro de I.A. Clássica / Simbólica e Satisfação de Restrições.