Near-Optimal Encodings of Cardinality Constraints

Resumo Técnico: Codificações Near-Ótimas para Restrições de Cardinalidade

1. O Problema

As restrições de cardinalidade são blocos fundamentais na teoria da satisfação booleana (SAT). Elas afirmam que, de um conjunto de variáveis booleanas $x_1, \dots, x_n$, no máximo $k$ delas podem ser verdadeiras. A restrição mais básica é AtMostOne ($k=1$).

O desafio central é codificar essas restrições em Forma Normal Conjuntiva (CNF) de forma eficiente. Uma codificação ingênua para AtMostOne requer $\binom{n}{2}$ cláusulas (complexidade quadrática), o que é inviável para grandes $n$. Embora existam codificações lineares ($O(n)$) que introduzem variáveis auxiliares, a questão de qual é o número mínimo de cláusulas necessário para uma codificação (especialmente uma que seja completa de propagação, garantindo consistência de arco via propagação de unidades) permaneceu em aberto ou baseada em conjecturas.

O artigo aborda duas questões principais:

1. Refutar a conjectura de que a codificação de produto de Chen (2010) é ótima para AtMostOne.
2. Desenvolver novas codificações para AtMostk (onde $k$ é pequeno em relação a $n$) que superem os limites anteriores de tamanho.

2. Metodologia e Técnicas Propostas

Os autores introduzem três técnicas principais que formam a base de suas contribuições:

• Reinterpretação Gráfica de Codificações:
  A codificação de produto de Chen é tradicionalmente vista como uma grade bidimensional. Os autores a reinterpretam como um grafo bipartido completo, onde as variáveis de entrada são arestas e as variáveis auxiliares são vértices. Eles generalizam isso para grafos multipartidos completos. Ao aumentar o número de partições (de 2 para $\omega(1)$), eles conseguem aumentar a densidade de arestas, permitindo codificar o mesmo número de variáveis de entrada com menos vértices (variáveis auxiliares) e cláusulas.

• Compressão de Grade (Grid Compression):
  Inspirada em tabelas hash, esta técnica organiza as variáveis de entrada em uma grade $M$ e a "comprime" em uma grade menor $L$. O objetivo é garantir que, se no máximo $k$ variáveis em $M$ forem verdadeiras, então no máximo $k$ colunas em $L$ serão ocupadas. Isso é feito mapeando colunas ocupadas de $M$ para colunas de $L$ usando conjuntos de destino pequenos ($H_j$), resolvendo o problema de garantir que colunas distintas não colidam no mesmo destino (usando o Teorema do Casamento de Hall ou famílias de conjuntos livres de cobertura).

• Comutação Disjuntiva (Disjunctive Switching):
  Uma nova paradigma para codificar estruturas de controle do tipo "switch" (seleção de ramos) em CNF. Em vez de codificar todas as ramificações possíveis (o que soma o tamanho de todas as ramificações), a técnica usa cláusulas largas (disjunções) para afirmar que algum ramo será tomado, e depois impõe restrições para garantir que apenas o ramo condicionalmente válido seja executado. Isso permite reduzir o número de cláusulas de $C \cdot n$ para $n + o(n)$, onde $C$ é o número de condições.

3. Principais Contribuições e Resultados

A. Para AtMostOne ($k=1$):

• Refutação da Conjectura de Chen: Os autores apresentam uma codificação de grafos multipartidos que utiliza $2n + 2\sqrt{2n} + O(\sqrt[3]{n})$ cláusulas. Isso melhora a codificação de produto de Chen, que usava $2n + 4\sqrt{n} + O(\sqrt[4]{n})$ cláusulas.
• Novo Limite Inferior (Lower Bound): Eles provam que qualquer codificação de AtMostOne (mesmo sem assumir completude de propagação) requer pelo menos $2n + \sqrt{n} + 1 - 2$ cláusulas para $n \ge 8$. Este é o primeiro limite inferior não trivial incondicional para essa restrição, respondendo a uma questão aberta de Kučera, Savický e Vorel.
• Impacto em Complexidade de Circuitos: A construção fornece um circuito booleano monótono menor para a função threshold-2 (negação de AtMostOne), melhorando um resultado de 50 anos de Adleman e resolvendo uma questão aberta de 47 anos sobre a "conjectura de nível único" (single-level conjecture).

B. Para AtMostk ($k > 1$):

• Codificação de Compressão de Grade (Theorem 3): Para $k = o(n)$, oferece uma codificação com $4n + o(n)$ cláusulas.
• Codificação de Compressão de Grade Disjuntiva (Theorem 4): Combinando compressão de grade com comutação disjuntiva, para $k = o(\sqrt[3]{n})$, alcançam uma codificação de $2n + o(n)$ cláusulas.
• Generalização Disjuntiva (Theorem 7): Aplicando a comutação disjuntiva à codificação de produto generalizada, eles reduzem o tamanho de $(k+1)n + o(n)$ para $2n + O(k n^{k/(k+1)})$ cláusulas. Para $k$ fixo pequeno, isso resulta em $2n + o(n)$.

C. Resultados Empíricos:

• Embora as novas codificações (especialmente as de grade) não sejam completas de propagação (uma propriedade tradicionalmente considerada essencial para o desempenho dos solvers SAT), os experimentos mostram que elas podem ser competitivas na prática.
• Em instâncias "fáceis" (família L), a codificação de Compressão de Grade Disjuntiva (DGC) superou significativamente as codificações tradicionais em tempo de execução e número de cláusulas.
• Em instâncias difíceis (família M, variante do princípio da pombal), a falta de completude de propagação prejudicou o desempenho, sugerindo que a completude ainda é crucial para certos tipos de problemas, mas não é uma regra absoluta para todos os cenários.

4. Significado e Impacto

Este trabalho representa um avanço teórico significativo na teoria de codificações CNF:

1. Ótimo Assintótico: Estabelece que o número mínimo de cláusulas para AtMostOne é $2n + \Theta(\sqrt{n})$, fechando a lacuna entre limites superiores e inferiores.
2. Novas Ferramentas: Introduz técnicas (comutação disjuntiva, compressão de grade) que podem ser aplicadas a outros problemas de codificação booleana, desafiando a visão de que apenas codificações de 2-CNF ou completas de propagação são eficientes.
3. Conexão Interdisciplinar: Conecta problemas de SAT a complexidade de circuitos booleanos e teoria de grafos, resolvendo questões abertas em ambas as áreas.
4. Praticidade: Demonstra que codificações teoricamente menores, mesmo sem completude de propagação, podem oferecer vantagens práticas em termos de tamanho de fórmula e desempenho em solvers modernos, desafiando o "senso comum" da comunidade SAT.

Em suma, o artigo redefine os limites do que é possível em termos de compactação de restrições de cardinalidade, oferecendo tanto provas teóricas rigorosas quanto evidências empíricas de utilidade prática.