An Efficient Algorithm for Solving the 2-MAXSAT Problem

Technische Samenvatting: Een Efficiënt Algoritme voor het Oplossen van het 2-MAXSAT-probleem

Probleemdefinitie
Het artikel behandelt het 2-MAXSAT-probleem, een beperkte versie van het Maximum Satisfiability (MAXSAT) probleem. Gegeven een verzameling $V$ van $m$ Booleaanse variabelen en een collectie $C$ van $n$ clausules in Conjunctive Normal Form (CNF), waarbij elke clausule maximaal twee literalen bevat, is het doel om een waarheidstoewijzing te vinden die het aantal bevredigde clausules maximaliseert. Het probleem wordt vastgesteld als NP-volledig, zelfs onder deze beperking.

Methodologie
Het voorgestelde algoritme wijkt af van traditionele branch-and-bound of benaderingsmethoden door het probleem te transformeren naar een DNF-maximalisatietaak en gebruik te maken van een gespecialiseerde graafgebaseerde zoekstructuur. De methodologie verloopt via drie hoofdfasen:

1. Transformatie naar DNF:
   Het algoritme construeert een nieuwe formule $D$ in DNF vanuit de oorspronkelijke CNF-formule $C$. Voor elke clausule $C_i = l_{i1} \lor l_{i2}$ in $C$, introduceert het algoritme een nieuwe hulpvariabele $x_i$ en genereert het twee conjuncties: $D_{i1} = l_{i1} \land x_i$ en $D_{i2} = l_{i2} \land \neg x_i$. De resulterende formule $D$ bestaat uit $2n$ conjuncties. Propositie 1 in het artikel stelt vast dat $C$ ten minste $n^*$ bevredigde clausules heeft indien en slechts indien $D$ ten minste $n^*$ bevredigde conjuncties heeft onder een waarheidstoewijzing voor $V \cup \{x_1, \dots, x_n\}$.

2. Graafrepresentatie (p-grafen en Tries):*
   Om de waarheidstoewijzingen die de conjuncties in $D$ bevredigen efficiënt te representeren, introduceert het artikel de p-graaf*.

   • Variabele Sequenties: Elke conjunctie wordt omgezet in een gesorteerde variabele sequentie op basis van de globale frequentie van het voorkomen van variabelen. Negatieve literalen worden afgehandeld door een speciale notatie $(c, *)$ te introduceren, die aangeeft dat variabele $c$ zowel waar als onwaar kan zijn (of overgeslagen kan worden) zonder de waarheid van de conjunctie te beïnvloeden.
   • p-grafen: Een gerichte graaf die een enkele conjunctie representeert waarbij knopen overeenkomen met variabelen in de sequentie. "Spans" (randen die variabelen overslaan) representeren de $(c, *)$ opties.
   • p-grafen:* Een verfijning van p-grafen waarbij "overlappende spans" (consecutieve optionele variabelen) worden samengevoegd via transitieve afsluiting. Dit zorgt ervoor dat de graaf alle geldige waarheidstoewijzingen voor een specifieke conjunctie correct representeert.
   • Trie-achtige Structuur ($G$): Alle p*-grafen worden geïntegreerd in één enkele trie-achtige graaf $G$. Deze structuur clustert veelvoorkomende variabele sequenties om redundante controles te vermijden. De graaf bevat "vertakkingsknopen" waar paden uiteenlopen.

3. Recursieve Bottom-Up Zoektocht:
   Het kernalgoritme, SEARCH(G), verkent de graaf $G op een bottom-up (post-order) wijze om de maximale deelverzameling van bevredigde conjuncties te vinden.

   • Reachable Subsets (RS): Voor een vertakkingsknoop $v$ berekent het algoritme "reachable subsets" van knopen die bereikbaar zijn via spans van voorouders. Deze deelverzamelingen representeren groepen conjuncties die gelijktijdig bevredigd kunnen worden door bepaalde variabelen over te slaan.
   • Upper Boundaries (upBounds): Gebaseerd op RS'en identificeert het algoritme "upper boundaries"—verzamelingen van knopen die het samenvoegen van subgrafen mogelijk maken.
   • Recursieve Constructie: Wanneer een vertakkingsknoop wordt tegengekomen, construeert het algoritme een nieuwe, kleinere trie-achtige subgraaf geworteld in de knopen in de upper boundary. Een virtuele wortel (de oorspronkelijke vertakkingsknoop) wordt toegevoegd om de connectiviteit te behouden. Het algoritme roept SEARCH recursief aan op deze subgrafen.
   • Optimalisatie: Om redundante berekeningen te voorkomen, gebruikt het algoritme twee verbeteringen: (1) het beperken van RS-berekeningen tot het segment tussen de huidige vertakkingsknoop en de laagste voorouder-vertakkingsknoop, en (2) het gebruik van een hash-array om resultaten van eerder bezochte subgrafen te cachen, waardoor herhaalde recursieve oproepen worden onderdrukt.

Belangrijkste Bijdragen

• Transformatietechniek: Een polynomiale reductie van het 2-MAXSAT-probleem naar een maximum bevredigbaar conjunctieprobleem in DNF.
• p-graaf Structuur:* De definitie van p*-grafen en hun transitieve afsluiting om waarheidstoewijzingen voor conjuncties met optionele variabelen accuraat en compact te representeren.
• Recursieve Trie Zoektocht: Een nieuw recursief algoritme dat dynamisch een trie-achtige graafstructuur bouwt en doorzoekt, waarbij gebruik wordt gemaakt van "reachable subsets" en "upper boundaries" om oplossingsruimtes efficiënt samen te voegen.
• Complexiteitsanalyse: Het artikel biedt een gedetailleerde analyse die beweert dat het algoritme binnen polynomiale tijdsgrenzen opereert.

Resultaten en Complexiteit
Het artikel stelt dat de worst-case tijdcomplexiteit van het voorgestelde algoritme begrensd is door $O(n^2 m^4)$, waarbij $n$ het aantal clausules is en $m$ het aantal variabelen.

• De constructie van de initiële trie en p*-grafen neemt $O(nm^2)$ in beslag.
• De recursieve zoektocht omvat maximaal $O(nm)$ vertakkingsknopen.
• Elke vertakkingsknoop is betrokken bij maximaal $O(m)$ recursieve oproepen vanwege de reductie in graafhoogte bij elke stap.
• De kosten voor het construeren van een subgraaf per oproep is $O(nm^2)$.
• Het combineren van deze factoren levert de $O(n^2 m^4)$ grens op.

Betekenis en Claims
Het artikel concludeert dat aangezien het 2-MAXSAT-probleem bekend staat als NP-volledig, het bestaan van een polynomiale-tijd algoritme om het op te lossen een bewijs vormt dat P = NP. De auteurs stellen dat dit resultaat een bewijs levert voor P = NP, wat het begrip van computationele complexiteit voor verzadigingsproblemen fundamenteel verandert. Het werk wordt gepresenteerd als een modificatie en uitbreiding van een conferentiepaper, ondersteund door NSERC, Canada.