Satisfatibilidade Booleana e a Conexão com Cook-Levin

• Enunciar com precisão o problema SAT e explicar o que uma atribuição satisfatória e um resultado UNSAT significam, cada um, para uma pergunta de verificação.
• Converter pequenas fórmulas booleanas para a forma normal conjuntiva e explicar por que a CNF é o formato de entrada padrão para solvers.
• Explicar, no nível da intuição, por que o teorema de Cook-Levin torna as fórmulas booleanas expressivas o bastante para codificar computações limitadas.
• Codificar uma pequena pergunta de alcançabilidade limitada como uma consulta de satisfatibilidade booleana.
• Ligar o papel do SAT na verificação formal aos resultados sobre classes de complexidade já provados em Computabilidade e Complexidade.

Tudo o que foi construído até aqui no bloco de lógica de Hoare desta disciplina (triplas, regras de inferência, invariantes, variantes, precondições mais fracas) é um método para construir provas, mas deixou em aberto como exatamente os passos lógicos individuais dentro dessas provas são checados quando envolvem raciocínio aritmético ou combinatório não trivial. O SAT é onde começa a metade automatizada desta disciplina, e ele fica em um ponto de encontro genuinamente central de três áreas que este currículo já cobriu separadamente: a lógica fornece a linguagem em que uma fórmula é escrita, a teoria da complexidade fornece o motivo de levar o SAT a sério como o problema difícil canônico, e a verificação formal fornece o uso prático: reduzir uma obrigação de prova à pergunta única e bem definida de se alguma fórmula booleana tem uma atribuição satisfatória.

A conexão com Computabilidade e Complexidade, estabelecida lá por completo, é direta aqui, e não incidental: NP é definida como a classe de problemas cujas respostas "sim" têm certificados checáveis em tempo polinomial, e o SAT é o problema NP-completo canônico; o teorema de Cook-Levin, que este conceito desenvolve no nível da intuição, é exatamente a prova de que o SAT é pelo menos tão difícil quanto todo outro problema de NP, porque todo problema de NP pode ser codificado como uma instância de SAT de tamanho comparável. Essa codificação não é uma curiosidade abstrata confinada à teoria da complexidade; é o mecanismo literal que as ferramentas de verificação formal exploram em escala de engenharia, traduzindo execuções limitadas de programas, aritmética de bit-vectors e escolhas combinatórias finitas diretamente em fórmulas booleanas sobre as quais um solver SAT pode então buscar automaticamente.

SAT

O problema da satisfatibilidade booleana, SAT, recebe como entrada uma fórmula booleana construída com variáveis e os conectivos já familiares de Matemática Discreta e Lógica, e faz uma única pergunta de sim ou não: existe alguma atribuição de true/false a cada variável que faça a fórmula inteira ser avaliada como true? Uma resposta "sim" vem com um certificado trivial de checar (a própria atribuição satisfatória, que pode ser aplicada direto à fórmula e avaliada em tempo proporcional ao tamanho da fórmula, sem nenhuma esperteza necessária para confirmá-la). Uma resposta "não", convencionalmente chamada de UNSAT, é uma afirmação muito mais forte e valiosa para fins de verificação do que pode parecer à primeira vista: ela diz que literalmente nenhuma atribuição de valores-verdade, em todo o espaço (exponencialmente grande) de atribuições possíveis, satisfaz a fórmula, o que, em um contexto de verificação, muitas vezes corresponde precisamente a uma ausência provada de contraexemplos; exatamente a conexão que logic-for-specification-propositional-and-first-order estabeleceu ao mostrar que a consequência lógica pode ser checada testando se uma negação é insatisfatível.

CNF e cláusulas

A maioria dos solvers SAT práticos é projetada para operar especificamente sobre fórmulas em forma normal conjuntiva: um E de cláusulas, em que cada cláusula é um OU de literais (uma variável ou sua negação). Esse formato restrito não é uma perda de expressividade de nenhum modo que importe para os propósitos do solver: qualquer fórmula booleana pode ser transformada em uma fórmula CNF equissatisfatível (que é satisfatível exatamente quando a original é, mesmo que não seja logicamente idêntica a ela), normalmente introduzindo variáveis auxiliares que nomeiam subexpressões intermediárias, em vez de por uma explosão de tamanho. O motivo de a CNF ser o formato-alvo padrão é prático, e não teórico: ela dá aos solvers um padrão estrutural único e uniforme (uma conjunção de restrições independentes, cada uma individualmente simples) em torno do qual os algoritmos de busca e de análise de conflitos dos solvers SAT modernos são especificamente projetados.

A intuição de Cook-Levin

A prova do teorema de Cook-Levin funciona mostrando que toda a execução limitada de qualquer computação não determinística em tempo polinomial pode ser codificada como um tableau: conceitualmente, uma grade cujas linhas representam momentos sucessivos no tempo e cujas colunas representam posições na fita da máquina ou componentes da sua configuração. Restrições de consistência local, cada uma envolvendo só uma vizinhança pequena e fixa de células da grade, forçam cada linha a decorrer corretamente da linha logo acima dela segundo as regras de transição reais da máquina; nenhuma restrição individual precisa "enxergar" a computação inteira de uma vez, só a própria pequena vizinhança local. O ganho crucial dessa construção: uma atribuição satisfatória da fórmula booleana resultante corresponde exatamente a um histórico de computação de aceitação válido da máquina original em alguma entrada e, inversamente, uma computação de aceitação genuína, codificada corretamente, satisfaz a fórmula; essa correspondência é o que torna a estrutura de um problema eficientemente checável totalmente expressável como uma fórmula booleana de tamanho comparável, e é o coração técnico de por que o SAT pode servir como alvo universal de codificação.

Uso na verificação

As ferramentas de verificação formal exploram exatamente essa mesma ideia de codificação em um nível muito mais concreto e voltado à engenharia do que a construção abstrata do tableau. O bounded model checking é o caso paradigmático: em vez de explorar o comportamento completo, possivelmente infinito, de um sistema, ele codifica todo caminho de execução possível de algum comprimento fixo e limitado k como uma única fórmula booleana, em que as variáveis representam os valores do estado do programa ou do sistema em cada um dos k passos de tempo e as restrições codificam tanto a relação de transição (como o estado no tempo t determina o estado no tempo t+1) quanto a propriedade sendo checada. Perguntar se um estado ruim é alcançável dentro desse limite vira então exatamente uma consulta SAT: se a fórmula codificada for satisfatível, existe um bug dentro de k passos, e se for insatisfatível, não existe bug dentro desse limite específico (embora possa existir além dele, uma limitação a que state-space-explosion-and-symbolic-model-checking e the-limits-of-verification voltam explicitamente). Quando a fórmula se mostra satisfatível, a atribuição retornada não é só um "sim" abstrato: ela se decodifica diretamente em um rastro concreto, passo a passo, da execução problemática, dando a um engenheiro exatamente o tipo de contraexemplo concreto que testing-shows-presence-proof-shows-absence já identificou como mais útil que um relatório abstrato de prova que falhou.

Fórmula pequena

Considere a fórmula (a ∨ b) ∧ (¬a ∨ c), já em CNF como uma conjunção de duas cláusulas. Tente a atribuição a = true, b = false, c = true. Checando a primeira cláusula, a ∨ b: como a é verdadeiro, a disjunção é verdadeira qualquer que seja o valor de b. Checando a segunda cláusula, ¬a ∨ c: ¬a é falso (já que a é verdadeiro), mas c é verdadeiro, então a disjunção é verdadeira pelo segundo termo. As duas cláusulas são avaliadas como verdadeiras, então a conjunção delas, a fórmula inteira, é avaliada como verdadeira sob esta atribuição, confirmando que a fórmula é satisfatível, com esta atribuição específica servindo como o certificado testemunha que torna trivial checar a resposta "sim", exatamente como a seção de Teoria Central descreveu.

Alcançabilidade como SAT

Considere modelar um sistema minúsculo com uma variável de estado booleana s que significa "o sistema está no estado Busy", ao longo de dois passos de tempo, s0 (inicial) e s1 (depois de uma transição), junto com uma entrada de controle start0 no tempo 0. Codifique o modelo como três restrições: a restrição de estado inicial s0 = false (o sistema começa ocioso, não ocupado); a restrição de transição s1 = true exatamente quando start0 = true (um sinal start no tempo 0 causa o estado ocupado no tempo 1); e a restrição de estado ruim sendo checada, s1 = true (a propriedade em teste é "Busy é alcançável no tempo 1?"). Conjuntar essas restrições em uma única fórmula e perguntar se ela é satisfatível é precisamente a versão codificada em SAT da pergunta de alcançabilidade. Uma atribuição satisfatória com start0 = true (e o resto das variáveis definido de forma consistente com a restrição de transição) é exatamente um contraexemplo de um passo: ela demonstra concretamente, pelos valores atribuídos, que começar ocioso e receber um sinal start de fato leva ao estado Busy; uma testemunha genuína de alcançabilidade, produzida automaticamente por um solver SAT de uso geral, sem nenhum código sob medida de busca de alcançabilidade.

UNSAT como prova

Considere um protocolo cuja propriedade de segurança pretendida é "nenhum estado é ao mesmo tempo Locked e Unlocked", modelado com um invariante booleano Unlocked ↔ ¬Locked que restringe as duas variáveis de estado a serem sempre opostas exatas. Para checar a propriedade de segurança procurando um contraexemplo, codifique a conjunção Locked ∧ Unlocked (a combinação ruim literal sendo procurada) junto com o invariante Unlocked ↔ ¬Locked e pergunte se a fórmula resultante é satisfatível. Como o invariante força Unlocked e Locked a sempre terem valores-verdade opostos, nenhuma atribuição consegue tornar Locked e Unlocked verdadeiros ao mesmo tempo: a fórmula é UNSAT. Esse resultado UNSAT não é só "o solver não achou um estado ruim e desistiu"; é uma prova completa, sobre todo o espaço exaustivo de atribuições booleanas possíveis, de que a combinação ruim é genuinamente impossível sob o modelo enunciado; exatamente o tipo de prova por busca exaustiva que testing-shows-presence-proof-shows-absence distinguiu dos testes baseados em amostragem logo no início desta disciplina, agora realizada concretamente por um solver em vez de por uma derivação simbólica em lógica de Hoare.

• Pensar que NP significa "não polinomial" em vez de "certificados checáveis em tempo polinomial". É uma armadilha puramente terminológica, mas persistente: problemas NP não são necessariamente difíceis de resolver em algum sentido absoluto; eles são definidos por quão rápido uma solução proposta pode ser verificada, e não por quão rápido uma solução pode ser encontrada, e a NP-completude do SAT é uma afirmação sobre o tempo de verificação, não sobre a impossibilidade de resolver instâncias de forma eficiente na prática.
• Confundir SAT com validade. O SAT pergunta se alguma atribuição satisfaz a fórmula, uma pergunta existencial comparativamente fraca, enquanto a validade (de logic-for-specification-propositional-and-first-order) pergunta se toda atribuição a satisfaz, uma afirmação universal muito mais forte. São relacionadas, mas distintas: é a negação de uma fórmula ser UNSAT que corresponde à fórmula original ser válida, e não a própria fórmula ser SAT.
• Esquecer que codificações limitadas só cobrem o número de passos escolhido. Um resultado de bounded model checking que não encontra estado ruim dentro de k passos não diz absolutamente nada sobre o passo k+1 ou além; esse limite é uma limitação genuína e explícita da técnica, e não um descuido, e é exatamente a tensão a que the-limits-of-verification volta ao distinguir evidência correta, porém limitada, de uma prova totalmente geral.
• Presumir que um modelo SAT de inteiros de máquina se comporta exatamente como inteiros matemáticos. Codificar aritmética em variáveis booleanas exige decidir exatamente como os números são representados (bit-vectors de largura fixa, por exemplo), e uma codificação de largura fixa pode exibir comportamento de wraparound e overflow que um modelo idealizado de inteiros matemáticos nunca mostraria; smt-solvers-and-decision-procedures desenvolve em detalhe essa distinção entre bit-vector e inteiro com um exemplo concreto de overflow.

O SAT reduz uma pergunta de verificação finita e bem definida (uma codificação booleana de alguma obrigação de prova ou execução limitada tem uma atribuição satisfatória?) a um único problema de busca bem definido, e o teorema de Cook-Levin explica, pela construção do tableau esboçada acima, por que essas codificações booleanas são expressivas o bastante para capturar computações limitadas arbitrárias, e é exatamente isso que torna o bounded model checking baseado em SAT possível como técnica de engenharia, e não como curiosidade teórica. Uma atribuição satisfatória se decodifica diretamente em um rastro de contraexemplo concreto, enquanto um resultado UNSAT é uma prova genuína e exaustiva de que uma propriedade limitada não é violada; os dois resultados carregam o tipo de peso exaustivo e estrutural que testing-shows-presence-proof-shows-absence distinguiu da mera amostragem logo no início desta disciplina. smt-solvers-and-decision-procedures continua diretamente daqui, estendendo esse mesmo mecanismo de busca booleana com raciocínio ciente de teorias sobre inteiros, arrays e bit-vectors, que o SAT puro sozinho não consegue expressar.