Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reintroducing the Second Player in EPR

Leroy Chew, Mikoláš Janota, Miroslav Olšák, Martin Suda

TL;DR

The main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy.

Abstract

In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (Effectively Propositional). While Bernays-Schoenfinkel is NEXPTIME-complete, we already can obtain fragments that are PSPACE-complete by restricting our clauses to DET-HORN or KROM. However such restrictions yield very different formulas to the canonical PSPACE-complete language of Quantified Boolean Formulas (QBF). This is despite Bernays-Schoenfinkel having a natural connection to an extension of QBF known as Dependency QBF. Our main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy. We use this definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy.

Reintroducing the Second Player in EPR

TL;DR

The main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy.

Abstract

In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (Effectively Propositional). While Bernays-Schoenfinkel is NEXPTIME-complete, we already can obtain fragments that are PSPACE-complete by restricting our clauses to DET-HORN or KROM. However such restrictions yield very different formulas to the canonical PSPACE-complete language of Quantified Boolean Formulas (QBF). This is despite Bernays-Schoenfinkel having a natural connection to an extension of QBF known as Dependency QBF. Our main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy. We use this definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy.
Paper Structure (7 sections, 12 theorems, 18 equations, 1 table, 1 algorithm)

This paper contains 7 sections, 12 theorems, 18 equations, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Observations on first-order logic
  4. Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF)
  5. A QBF-like fragment of Bernays-Schönfinkel
  6. Software and Experimentation
  7. Conclusion

Key Result

lemma 1

Suppose we have a CNF $\phi$ in the QEALM-fragment and for every $i\in \mathop{\mathrm{\mathsf{oPos}}}\limits(\phi)$, we have a constant symbol $c_i$. Let us build an instantiation $\sigma$ such that for every variable $u$ that appears in some argument $i\in \mathop{\mathrm{\mathsf{oPos}}}\limits(\p

Theorems & Definitions (32)

  • proof
  • definition 1: QBF-like EPR via Alternating Level-ordered Miniscoping (QEALM-fragment)
  • definition 2: Outer Variables
  • definition 3: Outer Position
  • lemma 1
  • proof
  • definition 4: Inseparable Clause
  • definition 5: Component
  • lemma 2
  • proof
  • ...and 22 more