Counting Quantifiers and the Stellar Fragment

This paper defines a class of clauses which we call the , and establishes that both the satisfiability and finite satisfiability problems for sets of stellar clauses are complete for nondeterministic exponential time. It is shown that the stellar fragment is closely related to the familiar two-variable fragment of first-order logic with counting quantifiers, . Our results thus demonstrate that finite satisfiability of -formulas is decidable in nondeterministic exponential time. Our method also yields a much easier proof of the previously known result that the satisfiability of -formulas is decidable in nondeterministic exponential time