1. A revolução algorítmica silenciosa da ciência da computação

Abra quase qualquer livro de ciência da computação teórica e você encontrará um aviso solene: «O Problema da Satisfatibilidade Booleana (SAT) é NP-completo. Como sua complexidade de tempo no pior caso cresce exponencialmente como \(O(2^n)\) em relação ao número de variáveis \(n\), instâncias grandes são fundamentalmente intratáveis.»

Do ponto de vista puramente combinatório, o argumento parece irrefutável. Uma fórmula proposicional sobre \(n = 100\) variáveis booleanas admite \(2^{100} \approx 1.26 \times 10^{30}\) atribuições de verdade possíveis. Mesmo que um supercomputador pudesse verificar \(10^{12}\) atribuições por segundo desde o Big Bang (há 13,8 bilhões de anos), teria explorado menos de \(10^{-8}\) do espaço de busca até hoje. De fato, por volta de 1990, os melhores solucionadores SAT travavam diante de fórmulas com apenas \(100\) variáveis e \(400\) cláusulas.

No entanto, no século XXI, a engenharia desafia essa intuição milhões de vezes por dia. Solucionadores SAT e SMT industriais modernos — como MiniSat, Glucose, Lingeling, CaDiCaL, Kissat e o Z3 da Microsoft Research — resolvem rotineiramente instâncias de verificação formal de microprocessadores, otimização de compiladores e resolução de dependências de pacotes com \(10.000.000\) (\(10^7\)) de variáveis e \(50.000.000\) (\(5 \times 10^7\)) de cláusulas em questão de segundos.

Quando Donald E. Knuth publicou o Volume 4B (Seção 7.2.2.2) de The Art of Computer Programming em 2015, dedicou mais de 300 páginas exclusivamente aos solucionadores SAT, saudando os avanços do final dos anos 1990 e início dos anos 2000 como uma das maiores revoluções algorítmicas da história da computação. Se antes reduzir um problema a SAT significava provar sua intratabilidade prática, hoje traduzir um problema combinatório difícil para SAT é a estratégia definitiva para resolvê-lo instantaneamente.

2. Forma Normal Conjuntiva (CNF), transformação de Tseitin e o teorema de Cook-Levin (1971)

2.1 Forma Normal Conjuntiva (CNF) e codificação linear de Tseitin

Um solucionador SAT opera sobre uma fórmula proposicional \(\Phi\) definida sobre \(n\) variáveis booleanas \(V = \{x_1, \dots, x_n\}\) com valores em \(\{0, 1\}\). Um literal \(\ell \in \{x_v, \neg x_v\}\) é uma variável ou sua negação; uma cláusula \(C_i = \bigvee_{j=1}^{k_i} \ell_{i,j}\) é uma disjunção (OR lógico, \(\lor\)) de literais; e uma fórmula na Forma Normal Conjuntiva (CNF) é uma conjunção (AND lógico, \(\land\)) de \(m\) cláusulas:

Se convertêssemos ingenuamente um circuito lógico arbitrário para CNF aplicando repetidamente a lei distributiva \(A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)\), o tamanho da fórmula explodiria exponencialmente. Em 1968, Grigori Tseitin eliminou essa explosão com a transformação de Tseitin: introduz-se uma nova variável auxiliar \(y_g\) para a saída de cada porta lógica \(g\) do circuito e codifica-se a equivalência local \(y_g \leftrightarrow \text{porta}(a, b)\) com apenas 3 ou 4 cláusulas. Por exemplo, uma porta AND \(y_g \leftrightarrow (a \land b)\) equivale exatamente a três cláusulas:

Assim, qualquer circuito com \(|G|\) portas é convertido em tempo e espaço estritamente lineares \(O(|G|)\) em uma fórmula 3-CNF equissatisfatível.

2.2 O teorema de Cook-Levin e o abismo de complexidade entre 2-SAT e 3-SAT

Em 1971, Stephen Cook e Leonid Levin provaram independentemente o teorema de Cook-Levin: todo problema de decisão na classe \(\text{NP}\) pode ser reduzido em tempo polinomial a SAT codificando o quadro de computação espaço-temporal de uma máquina de Turing não determinística durante \(p(n)\) passos (estados \(S_{t,q}\), posição da cabeça \(H_{t,i}\), símbolos de fita \(T_{t,i,\sigma}\)) como uma fórmula CNF.

Quando cada cláusula possui no máximo \(k\) literais (\(k\)-SAT), existe um abismo entre \(k = 2\) e \(k = 3\):

• 2-SAT é resolvido em tempo linear \(O(n + m)\): uma cláusula binária \((\ell_1 \lor \ell_2)\) equivale a duas implicações direcionadas determinísticas \((\neg \ell_1 \Rightarrow \ell_2) \land (\neg \ell_2 \Rightarrow \ell_1)\). No grafo de implicação sobre os \(2n\) literais, o algoritmo de Tarjan calcula as componentes fortemente conexas (SCC) em tempo \(O(n+m)\): a fórmula é satisfatível se e somente se nenhuma variável \(x_v\) pertence à mesma SCC que \(\neg x_v\).
• 3-SAT é NP-completo: uma cláusula ternária \((\ell_1 \lor \ell_2 \lor \ell_3)\) equivale a \((\neg \ell_1 \land \neg \ell_2) \Rightarrow \ell_3\), uma hiperaresta que exige duas premissas simultâneas. Sob a Hipótese do Tempo Exponencial (ETH), nenhum algoritmo determinístico resolve 3-SAT em tempo subexponencial \(2^{o(n)}\) no pior caso.

3. O algoritmo DPLL clássico (1962) e a tragédia do backtracking cronológico

O algoritmo DPLL (Davis, Putnam, Logemann, Loveland, 1962) combina busca em profundidade com a propagação unitária (Unit Propagation / Boolean Constraint Propagation, BCP):

Propagação Unitária (BCP): Se sob a atribuição parcial atual todos os literais de uma cláusula \(C = (\ell_1 \lor \dots \lor \ell_{k-1} \lor \ell_k)\) exceto \(\ell_k\) forem avaliados como False (\(0\)) e \(\ell_k\) permanecer não atribuído, \(C\) é uma cláusula unitária. O solucionador força imediatamente \(\ell_k = \text{True}\) (\(1\)), disparando uma cascata em dominó de novas propagações unitárias até a saturação ou até falsificar todos os literais de alguma cláusula (Conflito).

Por que o DPLL esbarrava na barreira de 100 variáveis? Por causa do backtracking cronológico. Se o solucionador define \(x_1 = 0\) no nível de decisão \(d = 1\), faz 48 escolhas totalmente independentes \(x_2, \dots, x_{49}\) nos níveis \(d = 2 \dots 49\), e no nível \(d = 50\) escolhe \(x_{50} = 1\), gerando um conflito imediato causado unicamente por \(x_1 = 0\) e \(x_{50}\) através das cláusulas \((x_1 \lor \neg x_{50} \lor \pm x_{51})\) e \((x_1 \lor x_{50} \lor \pm x_{52})\), o DPLL recua apenas um nível para \(d = 49\), inverte a variável inocente \(x_{49}\) e repete exatamente o mesmo fracasso em \(2^{48} \approx 2.81 \times 10^{14}\) subárvores inúteis (thrashing)!

4. A revolução CDCL: grafos de implicação, resolução 1-UIP e salto não cronológico

Introduzido no GRASP (Marques-Silva & Sakallah, 1996) e consagrado no Chaff (Moskewicz et al., 2001), o Aprendizado de Cláusulas Dirigido por Conflitos (CDCL) transformou cada contradição em aprendizado permanente.

  flowchart TD
    Start["Entrada: Fórmula CNF Φ (Nível de decisão d = 0)"] --> BCP["Propagação de Restrições Booleanas (BCP)<br/>Propagação rápida via Dois Literais Vigiados (2WL)"]
    BCP --> CheckConflict{"Cláusula de conflito κ<br/>falsificada?"}
    CheckConflict -- "Sem conflito" --> CheckAllAssigned{"Todas as variáveis<br/>atribuídas?"}
    CheckAllAssigned -- "Sim" --> SAT["SATISFATÍVEL (SAT)<br/>Retornar atribuição σ"]
    CheckAllAssigned -- "Não" --> Branch["Ramificação (Decision): d ← d + 1<br/>Escolher variável com máxima atividade VSIDS<br/>Atribuir polaridade via Phase Saving"]
    Branch --> BCP
    CheckConflict -- "Sim (Conflito!)" --> CheckLevelZero{"No nível raiz<br/>d == 0?"}
    CheckLevelZero -- "Sim" --> UNSAT["INSATISFATÍVEL (UNSAT)<br/>Emitir certificado de prova DRAT"]
    CheckLevelZero -- "Não (d > 0)" --> Analyze["Análise de Conflito (Resolução 1-UIP)<br/>Percorrer o grafo de implicação para trás a partir de κ<br/>Resolver até restar apenas 1 literal do nível d (First UIP)"]
    Analyze --> Learn["Aprender Cláusula e Incrementar VSIDS<br/>Adicionar C_learned ao banco (calcular LBD)<br/>Aumentar atividade VSIDS das variáveis resolvidas"]
    Learn --> Backjump["Salto Não Cronológico (Backjump)<br/>Saltar diretamente ao Nível de Asserção d_back (2.º maior nível em C_learned)<br/>C_learned dispara imediatamente como cláusula unitária no BCP!"]
    Backjump --> BCP

4.1 Grafo de implicação, resolução booleana e o Primeiro Ponto de Implicação Único (1-UIP)

Cada literal atribuído \(\ell@d\) registra seu nível de decisão \(d\) e sua cláusula antecedente (razão) \(\text{reason}(\ell)\). Quando \(\kappa\) é falsificada, o CDCL inicializa \(C \leftarrow \kappa\) e percorre para trás a pilha de atribuições (Trail) no nível atual \(d_{\text{curr}}\), aplicando iterativamente a regra de resolução booleana:

No grafo de implicação, um vértice \(u@d_{\text{curr}}\) é um Ponto de Implicação Único (UIP) se todo caminho direcionado da decisão \(\ell_{\text{dec}}@d_{\text{curr}}\) até o conflito \(\Lambda\) passa obrigatoriamente por \(u\) (dominador). O UIP mais próximo do conflito é o Primeiro UIP (1-UIP), alcançado no exato instante em que a cláusula de trabalho \(C\) contém apenas um único literal pertencente ao nível de decisão atual \(d_{\text{curr}}\)!

Com \(x_1 = 0@1, x_2 = 0@2, x_3 = 1@3\), a decisão \(x_4 = 1@5\) e as cláusulas \(\omega_1 = (x_1 \lor \neg x_4 \lor x_5)\), \(\omega_2 = (\neg x_4 \lor \neg x_5 \lor x_6)\), \(\omega_3 = (x_2 \lor \neg x_6 \lor x_7)\), \(\omega_4 = (\neg x_3 \lor \neg x_6 \lor x_8)\) gerando o conflito \(\kappa = (\neg x_7 \lor \neg x_8)\), duas etapas de resolução de \(\kappa\) com \(\omega_4\) (pivô \(x_8\)) e \(\omega_3\) (pivô \(x_7\)) produzem a cláusula aprendida 1-UIP:

4.2 Salto não cronológico (Backjumping) e nível de asserção

Como os níveis em \(C_{\text{learned}}\) são \(\{5, 3, 2\}\), o solucionador salta diretamente para o segundo nível de decisão mais alto (nível de asserção) \(d_{\text{back}} = 3\)! No nível \(3\), \(x_2@2\) e \(\neg x_3@3\) continuam falsos enquanto \(\neg x_6\) volta a ficar livre, fazendo com que \(C_{\text{learned}}\) atue imediatamente como cláusula unitária assertiva e force \(\neg x_6 = 1@3\) (\(x_6 = 0@3\)) via BCP!

5. Milagres de engenharia: Dois Literais Vigiados (2WL), VSIDS e LBD

1. Dois Literais Vigiados (Two-Watched Literals, 2WL, Chaff 2001): Enquanto uma cláusula tiver pelo menos dois literais não falsificados, ela nunca poderá se tornar unitária nem conflitante. O solucionador vigia apenas dois literais \(w_1, w_2\) por cláusula. Ao realizar um backjump, desatribuir variáveis preserva automaticamente o invariante 2WL: o backtracking exige exatamente zero atualizações de ponteiros (\(O(1)\))!
2. VSIDS (Variable State Independent Decaying Sum) e Phase Saving: Variáveis envolvidas na resolução de conflitos recebem um bônus \(+\Delta\), enquanto \(\Delta \leftarrow \Delta / \gamma\) (\(\gamma = 0.95\)) cresce após cada conflito, focando a busca no gargalo ativo.
3. LBD (Literal Block Distance / Cláusulas «Glue») e reinícios rápidos: O Glucose (Audemard & Simon, 2009) define \(\text{LBD}(C)\) como o número de níveis de decisão distintos em \(C\). Cláusulas com \(\text{LBD} = 2\) (Glue Clauses) conectam diretamente o UIP atual a um único bloco passado e são mantidas permanentemente.

6. Implementação completa em Python de um motor CDCL

Abaixo está uma implementação completa em Python de um solucionador CDCL com BCP, grafo de implicação, resolução 1-UIP, salto não cronológico e VSIDS:

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112

from typing import List, Dict, Optional, Set, Tuple

class CDCLSolver:
    '''Minimal Conflict-Driven Clause Learning (CDCL) SAT Solver with 1-UIP & VSIDS.'''
    def __init__(self, num_vars: int, clauses: List[List[int]]):
        self.num_vars = num_vars
        self.clauses: List[List[int]] = [list(set(c)) for c in clauses]
        self.assigns: Dict[int, bool] = {}
        self.trail: List[int] = []
        self.level: Dict[int, int] = {}
        self.reason: Dict[int, Optional[List[int]]] = {}
        self.decision_level: int = 0
        self.activity: Dict[int, float] = {v: 0.0 for v in range(1, num_vars + 1)}
        for c in self.clauses:
            for lit in c:
                self.activity[abs(lit)] += 1.0
        self.var_inc: float = 1.0
        self.var_decay: float = 0.95

    def value_lit(self, lit: int) -> Optional[bool]:
        var = abs(lit)
        if var not in self.assigns:
            return None
        return self.assigns[var] if lit > 0 else not self.assigns[var]

    def assign(self, lit: int, level: int, reason: Optional[List[int]]) -> None:
        var = abs(lit)
        self.assigns[var] = (lit > 0)
        self.trail.append(lit)
        self.level[var] = level
        self.reason[var] = reason

    def bcp(self) -> Optional[List[int]]:
        changed = True
        while changed:
            changed = False
            for clause in self.clauses:
                unassigned_lit = None
                num_unassigned = 0
                satisfied = False
                for lit in clause:
                    val = self.value_lit(lit)
                    if val is True:
                        satisfied = True
                        break
                    elif val is None:
                        num_unassigned += 1
                        unassigned_lit = lit
                if satisfied:
                    continue
                if num_unassigned == 0:
                    return clause
                if num_unassigned == 1 and unassigned_lit is not None:
                    self.assign(unassigned_lit, self.decision_level, clause)
                    changed = True
        return None

    def analyze_conflict(self, conflict_clause: List[int]) -> Tuple[List[int], int]:
        learned: Set[int] = set(conflict_clause)
        def count_curr_level(cset: Set[int]) -> int:
            return sum(1 for lit in cset if self.level[abs(lit)] == self.decision_level)

        idx = len(self.trail) - 1
        while count_curr_level(learned) > 1:
            while True:
                pivot_lit = self.trail[idx]
                idx -= 1
                if -pivot_lit in learned and self.level[abs(pivot_lit)] == self.decision_level:
                    break
            pivot_var = abs(pivot_lit)
            antecedent = self.reason[pivot_var]
            assert antecedent is not None
            self.activity[pivot_var] += self.var_inc
            learned.remove(-pivot_lit)
            for lit in antecedent:
                if lit != pivot_lit:
                    learned.add(lit)

        learned_clause = list(learned)
        for lit in learned_clause:
            self.activity[abs(lit)] += self.var_inc
        self.var_inc /= self.var_decay
        levels = sorted({self.level[abs(lit)] for lit in learned_clause}, reverse=True)
        backjump_level = levels[1] if len(levels) > 1 else 0
        return learned_clause, backjump_level

    def backtrack(self, target_level: int) -> None:
        while self.trail and self.level[abs(self.trail[-1])] > target_level:
            lit = self.trail.pop()
            var = abs(lit)
            del self.assigns[var], self.level[var], self.reason[var]
        self.decision_level = target_level

    def solve(self) -> Tuple[bool, Optional[Dict[int, bool]]]:
        if self.bcp() is not None:
            return False, None
        while True:
            unassigned = [v for v in range(1, self.num_vars + 1) if v not in self.assigns]
            if not unassigned:
                return True, dict(self.assigns)
            branch_var = max(unassigned, key=lambda v: self.activity[v])
            self.decision_level += 1
            self.assign(branch_var, self.decision_level, reason=None)
            while True:
                conflict = self.bcp()
                if conflict is None:
                    break
                if self.decision_level == 0:
                    return False, None
                learned_clause, backjump_level = self.analyze_conflict(conflict)
                self.clauses.append(learned_clause)
                self.backtrack(backjump_level)

7. Física estatística e a transição de fase do \(k\)-SAT aleatório (\(\alpha_c \approx 4.267\))

Em uma fórmula 3-SAT aleatória com \(n\) variáveis e \(m = \alpha n\) cláusulas (densidade \(\alpha = m / n\)), o método do primeiro momento fornece o valor esperado do número de soluções \(\mathbb{E}[Z]\):

Por meio do método da cavidade e da quebra de simetria de réplicas de um passo (1RSB) da física de vidros de spin, Mézard, Parisi e Zecchina (2002) determinaram o limiar crítico exato do 3-SAT aleatório:

  flowchart TD
    subgraph PhaseTransition["Transição de fase do 3-SAT aleatório conforme a densidade α = m/n"]
        S1["1. Fase líquida sub-restrita (α < 3.86 : Easy-SAT)<br/>• As soluções formam um único aglomerado gigante conectado em {0,1}^n<br/>• Resolução rápida em tempo polinomial"]
        S2["2. Fase vítrea de fragmentação e congelamento (3.86 < α < 4.267 : Hard-SAT)<br/>• Em α_d ≈ 3.86 (transição 1RSB), o espaço de soluções se despedaçada em exponencialmente muitas ilhas isoladas!<br/>• Em α_f ≈ 4.254 as variáveis dentro de cada ilha ficam rigidamente congeladas (Freezing)"]
        S3["3. Limiar crítico de satisfatibilidade (α_c ≈ 4.267 : Pico máximo de dificuldade)<br/>• A probabilidade de SAT cai abruptamente de 1 para 0<br/>• Toda refutação por resolução exige comprimento exponencial 2^Ω(n) (Chvátal–Szemerédi)"]
        S4["4. Fase sobre-restrita (α > 4.267 : Easy-UNSAT)<br/>• A alta densidade de cláusulas gera contradições em baixa profundidade<br/>• O tamanho da prova diminui conforme α cresce"]
    end
    S1 -->|"α_d ≈ 3.86 (Fragmentação)"| S2
    S2 -->|"α_c ≈ 4.267 (Transição UNSAT)"| S3
    S3 -->|"α > 4.267 (Conflitos rasos)"| S4

Em \(\alpha_c \approx 4.267\), o hipergrafo aleatório é um grafo expansor sem gargalos locais, exigindo refutações por resolução de comprimento exponencial \(2^{\Omega(n)}\) (Chvátal & Szemerédi, 1988). Já os problemas industriais reais possuem estrutura modular e conjuntos «Backdoor» pequenos (Ansótegui et al. 2012; Williams, Gomes, Selman 2003), permitindo que o CDCL decomponha 10 milhões de variáveis em segundos.

8. Triunfos no mundo real e a prova matemática de 200 Terabytes

1. Matemática assistida por computador e a prova DRAT de 200 TB (Heule, Kullmann, Marek 2016): Usando Cube-and-Conquer, provaram que o Problema Booleano dos Ternos Pitagóricos (\(a^2 + b^2 = c^2\)) é satisfatível até \(N = 7824\) (SAT), mas insatisfatível em \(N = 7825\) (UNSAT), gerando um certificado formal DRAT de 200 Terabytes, além de resolverem o número de Schur \(S(5) = 160\) (2018) e a conjectura de Keller na dimensão 7 (2020).
2. Verificação formal de chips EDA (CEC e BMC): circuitos Miter (XOR entre especificação RTL e portas lógicas) garantem equivalência exata antes da fabricação de qualquer CPU/GPU moderna.
3. Gerenciadores de pacotes (Debian apt, Rust Cargo, Dart PubGrub, uv) e Solucionadores SMT (\(\text{DPLL}(T)\): Z3 e cvc5): acoplando CDCL a solucionadores de teorias de primeira ordem, impulsionam a execução simbólica e a verificação de segurança em nuvem (AWS Zelkova).