Color Structures and the Monotone Satisfiability Problem with Bounded Variable Occurrence

Resumo Técnico: Estruturas de Cores e o Problema de Satisfatibilidade Monótona com Ocorrência Limitada de Variáveis

Enunciado do Problema
Este artigo aborda a complexidade do problema Monotone 3-Sat-(≤k, 1), uma variante restrita do problema de Satisfatibilidade Booleana (SAT). Nesta classe, as fórmulas estão em Forma Normal Conjuntiva (CNF) onde:

1. Cada cláusula contém exatamente três literais.
2. A fórmula é monótona: cada cláusula consiste inteiramente de variáveis não negadas (positivas) ou inteiramente de variáveis negadas (negativas).
3. Cada variável ocorre exatamente uma vez em uma cláusula negativa e no máximo k vezes em cláusulas positivas.

O desafio específico resolvido por este trabalho refere-se aos casos onde $k \in \{3, 4\}$. Pesquisas anteriores estabeleceram que:

• Para $k \le 2$, o problema é trivial (todas as instâncias são satisfatíveis) via o resultado de Tovey.
• Para $k \ge 5$, o problema é NP-completo (Darmann e Döcker).
• A complexidade para $k=3$ e $k=4$ permaneceu uma questão em aberto, representando o limiar preciso entre a satisfatibilidade garantida e a dificuldade computacional.

Metodologia: Estruturas de Cores
Para resolver os casos em aberto, os autores introduzem um novo arcabouço combinatório chamado estruturas de cores. A metodologia procede da seguinte forma:

1. Codificação via Cores: Como cada variável aparece exatamente uma vez negativamente, os autores codificam as cláusulas negativas atribuindo uma "cor" a todas as variáveis dentro de uma cláusula negativa específica. Variáveis que compartilham uma cor são chamadas de "parentes". As cláusulas negativas são efetivamente removidas da fórmula explícita, e suas restrições são carregadas pelo requisito de que exatamente uma variável por cor deve ser atribuída como falsa (um "guarda") para satisfazer a cláusula negativa original.
2. A Estrutura de Cores: Uma estrutura de cores é definida como um grafo $(G \cup N, E)$ onde:
   • $G$ é um conjunto de vértices guarda (variáveis atribuídas como falsas).
   • $N$ é um conjunto de vértices não-guarda (variáveis atribuídas como verdadeiras).
   • $E$ é um conjunto de arestas rotuladas representando cláusulas positivas. Uma aresta $\{u_i, v_j\}_{l_s}$ conecta duas variáveis $u_i$ e $v_j$ com um rótulo $l_s$, correspondendo a uma cláusula $(u_i \lor v_j \lor l_s)$.
   • A estrutura impõe que, se duas variáveis de uma cláusula estão em $G$, a terceira deve ser um rótulo de aresta; se uma está em $G$, as outras são distribuídas entre $N$ e rótulos de aresta.
3. Expansão e Bloqueio: O mecanismo algorítmico central envolve a expansão de variáveis (movê-las de $N$ para $G$). Uma variável é bloqueada se ela aparece em uma cláusula positiva onde as outras duas variáveis já são guardas. Uma cor é bloqueada se todas as suas variáveis estiverem bloqueadas. Uma atribuição satisfatória corresponde a uma estrutura de cores onde cada cor possui exatamente um guarda e nenhuma cor está totalmente bloqueada.
4. O Algoritmo: Os autores apresentam um algoritmo que expande avidamente as variáveis não guardadas, priorizando aquelas com o maior número de bloqueio (a contagem de parentes bloqueados). Se uma "cor bloqueada" (uma cor sem variáveis não guardadas disponíveis) é criada, o algoritmo entra em um loop interno para desexpandir (mover de volta para $N$) variáveis específicas para liberar um guarda para aquela cor. Este processo é modelado via um diagrama de estados envolvendo um "ciclo base" e "$\ell$-blocos".

Principais Contribuições e Resultados
A principal contribuição é a prova de que o Monotone 3-Sat-(k, 1) é trivial para $k \in \{3, 4\}$. Especificamente:

• Teorema 3.5: Toda fórmula Monotone 3-Sat onde cada variável ocorre uma vez negativamente e no máximo quatro vezes positivamente é satisfatível.
• Prova Construtiva: Os autores fornecem um algoritmo que constrói uma atribuição satisfatória em $O(n \cdot m)$ tempo, onde $n$ é o número de cláusulas negativas e $m$ é o número de cláusulas positivas.
• Teorema de Dicotomia (Corolário 3.6): O artigo estabelece uma dicotomia de complexidade completa para Monotone 3-Sat-(k, 1):
  • Trivial (Sempre Satisfatível): Para $1 \le k \le 4$.
  • NP-difícil: Para $k \ge 5$.

Significância e Alegações
O artigo afirma resolver um desafio específico proposto por Darmann e Döcker (2021) em relação ao hiato de complexidade entre $k=2$ e $k=5$. A significância do trabalho reside em:

1. Fechamento do Hiato de Complexidade: Ele define definitivamente o status dos casos $k=3$ e $k=4$, provando que eles não são NP-completos, mas sim subclasses triviais.
2. Visão Estrutural: A introdução das estruturas de cores fornece um novo olhar combinatório para analisar o SAT monótono. Os autores argumentam que este arcabouço captura a interação entre cláusulas positivas e negativas sob ocorrências limitadas de variáveis de forma mais eficaz do que as representações baseadas em grafos anteriores.
3. Precisão do Limiar: A prova baseia-se em um argumento de contagem comparando "lugares de prisioneiros" (locais disponíveis para variáveis bloqueadas) contra "parentes detentos" (variáveis que devem ser bloqueadas para forçar um estado específico). Os autores demonstram que para $k \le 4$, o número de lugares de prisioneiros é insuficiente para prender todas as variáveis necessárias, garantindo que o algoritmo sempre possa encontrar uma variável não guardada para expandir. Para $k \ge 5$, o argumento de contagem falha (suficientes lugares existem para prender as variáveis), o que se alinha com a NP-dureza conhecida do problema.
4. Eficiência Algorítmica: O resultado não é meramente existencial; ele fornece um método construtivo de tempo polinomial para encontrar a atribuição satisfatória, reforçando a "trivialidade" da classe.

Os autores concluem que, embora o conceito de estrutura de cores tenha sido desenvolvido para resolver este problema de limiar específico, ele pode ter relevância para outras abordagens de resolução de SAT, embora não proponham aplicações futuras específicas além deste escopo.