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).