Reintroducing the Second Player in EPR

Titel: Reintroducing the Second Player in EPR

Auteurs: Leroy Chew, Mikoláš Janota, Miroslav Olšák, en Martin Suda (Czech Technical University in Prague)

1. Probleemstelling en Context

Het artikel onderzoekt de computationele complexiteit van het satisfiability-probleem (SAT) voor sub-fragmenten van de Bernays-Schönfinkel-klasse (ook wel bekend als EPR - Effectively Propositional) van de eerste-orde logica.

• Achtergrond: De volledige Bernays-Schönfinkel-klasse is NEXPTIME-compleet, wat analoog is aan Dependency QBF (DQBF) in de propositional logica.
• Huidige beperkingen: Bestaande fragmenten die PSPACE-compleet zijn (zoals DET-HORN en KROM binnen EPR) hebben een zeer beperkte structuur. Hoewel ze PSPACE-compleet zijn, missen ze de natuurlijke eigenschappen van Quantified Boolean Formulas (QBF), zoals de duidelijke twee-speler spelsemantiek (universale vs. existentiële speler) en de manier waarop restricties leiden tot complete problemen binnen de polynoomhiërarchie.
• De kernvraag: Kan men een PSPACE-compleet fragment van Bernays-Schönfinkel definiëren dat een natuurlijk equivalent is van QBF, behoudt de twee-speler spelstructuur, en toch gesloten blijft onder resolutie?

2. Methodologie en Kernobservaties

De auteurs introduceren een nieuwe observatie over de structuur van onoplosbare (unsatisfiable) eerste-orde formules en bouwen hierop een nieuw fragment.

Observatie 1: De "Eerste Argument" Eigenschap

De auteurs stellen vast dat bij een onoplosbaar CNF-formulier (zonder gelijkheid) in de Bernays-Schönfinkel-klasse, er vaak een ground-term bestaat die als eerste argument fungeert in elk literaal binnen een clause.

• Als een clause $C$ een onoplosbaar bewijs heeft, kunnen de variabelen in de eerste positie van alle literaals in die clause worden geïnstancieerd naar een specifieke ground-term zonder de satisfiability te veranderen.
• Dit suggereert dat als de eerste argumenten van literaals binnen een clause consistent zijn, het probleem vereenvoudigd kan worden tot een geval dat lijkt op propositional logica, maar met een specifieke structuur die een spel tussen spelers mogelijk maakt.

Definitie van het QEALM-fragment

Op basis van deze observatie definiëren de auteurs het QEALM-fragment (QBF-like EPR via Alternating Level-ordered Miniscoping). Een Bernays-Schönfinkel-instance behoort tot dit fragment als:

1. In elke clause, als een variabele $u$ in meerdere literaals voorkomt, de eerste positie waarin deze voorkomt in alle literaals identiek is.
2. Voor alle posities $j$ tot en met de eerste positie van $u$, moeten de argumenten in die posities voor alle literaals gelijk zijn (een gedeeld initieel segment).

Dit creëert een structuur waar variabelen "forken" (uiteenlopen) op een bepaald punt, maar daarvoor gedeeld worden. Dit maakt het mogelijk om quantifiers te "miniscopen" (lokaal maken) en een spel tussen een universele en existentiële speler te simuleren.

3. Belangrijkste Bijdragen

1. Definitie van een Nieuw Fragment (QEALM):
   De auteurs definiëren een sub-fragment van Bernays-Schönfinkel dat PSPACE-compleet is en een directe vertaling is van QBF. Dit fragment behoudt de "twee-speler" spelsemantiek van QBF, waarbij de volgorde van quantifiers de strategie van de spelers bepaalt.

2. PSPACE-Completiteit en Hiërarchie:

   • Het fragment is bewezen PSPACE-compleet.
   • De auteurs introduceren het concept van "fork indices" (kruispunten waar variabelen uiteenlopen). Aantal en positie van deze indices bepalen de complexiteit binnen de polynoomhiërarchie:
     • Fragmenten met $k$ fork indices vallen in de complexiteitsklassen $\Sigma^P_{2k-1}$ of $\Pi^P_{2k}$.
   • Dit stelt onderzoekers in staat om problemen op verschillende niveaus van de polynoomhiërarchie te classificeren binnen EPR.

3. Sluiting onder Resolutie:
   In tegenstelling tot eerdere vertalingen van QBF naar EPR (zoals qbf2epr), is het QEALM-fragment gesloten onder de regels van Robinson's Resolutie. Dit is cruciaal voor het gebruik van bestaande theoremaprovers en bewijsvoering.

4. Robuustheid bij Restricties:
   Het fragment blijft PSPACE-hard (en dus compleet) zelfs wanneer het wordt gesneden met andere bekende fragmenten:

   • Krom (clauses met maximaal 2 literaals).
   • Horn (clauses met maximaal 1 positief literaal).
   • Affine (specifieke implicaties).
     Dit is opmerkelijk omdat QBF zelf deze eigenschappen niet altijd behoudt bij intersectie met deze fragmenten.

4. Resultaten en Experimenten

• Algoritme: De auteurs presenteren een recursief algoritme (SolveByAlternation) dat de satisfiability van QEALM-fragmenten beslist binnen PSPACE. Het algoritme wisselt af tussen een universele zoektocht (voor gedeelde variabelen) en een existentiële zoektocht (voor gescheiden componenten/clausules).
• TPTP Library Analyse:
  • De auteurs analyseerden 936 Bernays-Schönfinkel-problemen uit de TPTP bibliotheek (versie 9.1.0).
  • 308 problemen bleken tot het QEALM-fragment te behoren.
  • Deze omvatten:
    • 50 puur propositional problemen.
    • 109 monadische problemen.
    • 49 problemen met predicaten tot twee "variabele-actieve" argumentposities (vaak vertaalde ALC-problemen).
  • Problemen met hogere fork indices (complexer) werden geïdentificeerd in families zoals binaire tellers en geoptimaliseerde functionele vertalingen van modale QBF-formules.
• Limitaties: Het algoritme detecteerde 81 problemen die via qbf2epr waren gegenereerd niet direct als QEALM, hoewel ze na eliminatie van triviale clauses wel zouden passen.

5. Betekenis en Toekomstperspectief

• Theoretische Impact: Dit werk overbrugt de kloof tussen eerste-orde logica (EPR) en propositional logica (QBF). Het biedt een natuurlijk kader om PSPACE-compleetheid en de polynoomhiërarchie te bestuderen binnen de eerste-orde logica zonder de complexiteit van volledige DQBF.
• Praktische Toepassing: Omdat het fragment gesloten is onder resolutie, kunnen bestaande theoremaprovers (zoals Vampire) worden aangepast om deze fragmenten efficiënter op te lossen.
• Toekomstig Werk: De auteurs wijzen op de potentie voor bewijscomplexiteit (proof complexity). Hoewel Robinson's Resolutie exponentiële ondergrenzen heeft voor dit fragment (vergelijkbaar met "semantische hardheid" in QBF), biedt het een nieuwe testomgeving om bewijssystemen te bestuderen en te certificeren.

Conclusie:
Het artikel introduceert het QEALM-fragment als een fundamenteel nieuwe klasse binnen de eerste-orde logica. Het combineert de expressiviteit van EPR met de speltheoretische structuur van QBF, biedt een schaalbare manier om complexiteit binnen de polynoomhiërarchie te analyseren, en blijft compatibel met standaard resolutie-methoden, wat het een krachtig instrument maakt voor zowel theoretische logica als geautomatiseerd redeneren.