An Efficient Algorithm for Solving the 2-MAXSAT Problem

Resumo Técnico: Um Algoritmo Eficiente para Resolver o Problema 2-MAXSAT

Definição do Problema
O artigo aborda o problema 2-MAXSAT, uma versão restrita do problema de Satisfatibilidade Máxima (MAXSAT). Dada uma coleção $V$ de $m$ variáveis booleanas e uma coleção $C$ de $n$ cláusulas em Forma Normal Conjuntiva (CNF), onde cada cláusula contém no máximo dois literais, o objetivo é encontrar uma atribuição de verdade que maximize o número de cláusulas satisfeitas. O problema é estabelecido como NP-completo, mesmo sob esta restrição.

Metodologia
O algoritmo proposto afasta-se dos métodos tradicionais de branch-and-bound ou aproximação ao transformar o problema em uma tarefa de maximização de Forma Normal Disjuntiva (DNF) e utilizar uma estrutura de busca baseada em grafos especializada. A metodologia procede em três etapas principais:

1. Transformação para DNF:
   O algoritmo constrói uma nova fórmula $D$ em DNF a partir da fórmula CNF $C$ original. Para cada cláusula $C_i = l_{i1} \lor l_{i2}$ em $C$, o algoritmo introduz uma nova variável auxiliar $x_i$ e gera duas conjunções: $D_{i1} = l_{i1} \land x_i$ e $D_{i2} = l_{i2} \land \neg x_i$. A fórmula $D$ resultante consiste em $2n$ conjunções. A Proposição 1 do artigo estabelece que $C$ possui pelo menos $n^*$ cláusulas satisfatóveis se, e somente se, $D$ possui pelo menos $n^*$ conjunções satisfatóveis sob uma atribuição de verdade para $V \cup \{x_1, \dots, x_n\}$.

2. Representação em Grafo (p-grafos e Tries):*
   Para representar eficientemente as atribuições de verdade que satisfazem as conjunções em $D$, o artigo introduz o p-grafo*.

   • Sequências de Variáveis: Cada conjunção é convertida em uma sequência de variáveis ordenada com base na frequência global de aparição das variáveis. Literais negativos são tratados pela introdução de uma notação especial $(c, *)$, representando que a variável $c$ pode ser verdadeira ou falsa (ou ignorada) sem afetar a verdade da conjunção.
   • p-grafos: Um grafo direcionado que representa uma única conjunção onde os nós correspondem às variáveis na sequência. "Spans" (arestas que pulam variáveis) representam as opções $(c, *)$.
   • p-grafos:* Um refinamento dos p-grafos onde "spans sobrepostos" (variáveis opcionais consecutivas) são fundidos via fechamento transitivo. Isso garante que o grafo represente corretamente todas as atribuições de verdade válidas para uma conjunção específica.
   • Estrutura tipo Trie ($G$): Todos os p*-grafos são integrados em um único grafo do tipo trie $G$. Esta estrutura agrupa sequências comuns de variáveis para evitar verificações redundantes. O grafo inclui "nós de ramificação" onde os caminhos divergem.

3. Busca Recursiva Bottom-Up:
   O núcleo do algoritmo, SEARCH(G), explora o grafo $G$ de maneira ascendente (bottom-up, pós-ordem) para encontrar o subconjunto máximo de conjunções satisfatórias.

   • Subconjuntos Alcançáveis (RS): Para um nó de ramificação $v$, o algoritmo calcula "subconjuntos alcançáveis" de nós alcançáveis via spans a partir de ancestrais. Esses subconjertos representam grupos de conjunções que podem ser satisfeitas simultaneamente ao ignorar certas variáveis.
   • Limites Superiores (upBounds): Com base nos RSs, o algoritmo identifica "limites superiores" — conjuntos de nós que permitem a fusão de subgrafos.
   • Construção Recursiva: Quando um nó de ramificação é encontrado, o algoritmo constrói um novo subgrafo do tipo trie, menor, enraizado nos nós do limite superior. Uma raiz virtual (o nó de ramificação original) é adicionada para manter a conectividade. O algoritmo chama SEARCH recursivamente nestes subgrafos.
   • Otimização: Para evitar computação redundante, o algoritmo emprega duas melhorias: (1) limitando os cálculos de RS ao segmento entre o nó de ramificação atual e seu ancestral de ramificação mais baixo, e (2) utilizando um array de hash para fazer o cache dos resultados de subgrafos visitados anteriormente, suprimindo chamadas recursivas repetidas.

Principais Contribuições

• Técnica de Transformação: Uma redução de tempo polinomial do problema 2-MAXSAT para um problema de máxima conjunção satisfatória em DNF.
• Estrutura de p-grafo:* A definição de p*-grafos e seu fechamento transitivo para representar de forma precisa e compacta as atribuições de verdade para conjunções contendo variáveis opcionais.
• Busca em Trie Recursiva: Um novo algoritmo recursivo que constrói e busca dinamicamente uma estrutura de grafo do tipo trie, utilizando "subconjuntos alcançáveis" e "limites superiores" para fundir espaços de solução de forma eficiente.
• Análise de Complexidade: O artigo fornece uma análise detalhada alegando que o algoritmo opera dentro de limites de tempo polinomial.

Resultados e Complexidade
O artigo afirma que a complexidade de tempo de pior caso do algoritmo proposto é limitada por $O(n^2 m^4)$, onde $n$ é o número de cláusulas e $m$ é o número de variáveis.

• A construção da trie inicial e dos p*-grafos leva $O(nm^2)$.
• A busca recursiva envolve no máximo $O(nm)$ nós de ramificação.
• Cada nó de ramificação está envolvido em no máximo $O(m)$ chamadas recursivas devido à redução da altura do grafo em cada etapa.
• O custo para construir um subgrafo por chamada é $O(nm^2)$.
• Combinando esses fatores, obtém-se o limite de $O(n^2 m^4)$.

Significância e Alegações
O artigo conclui que, como o problema 2-MAXSAT é conhecido por ser NP-completo, a existência de um algoritmo de tempo polinomial para resolvê-lo constitui uma prova de que P = NP. Os autores afirmam que este resultado fornece uma prova de P = NP, alterando fundamentalmente a compreensão da complexidade computacional para problemas de satisfatibilidade. O trabalho é apresentado como uma modificação e extensão de um artigo de conferência, apoiado pelo NSERC, Canadá.