On the descriptive complexity of satisfiability on quantified Boolean formulas : a thesis presented in partial fulfilment of the requirements for the degree of Master of Information Sciences at Massey University, Wellington, New Zealand
Loading...
Date
2011
DOI
Open Access Location
Journal Title
Journal ISSN
Volume Title
Publisher
Massey University
Rights
The Author
Abstract
In the present thesis, we deal with the construction of non trivial formulas in higher
order logic languages. In particular, we focus on using SO (Second-Order logic) and
TO (Third-Order logic) to express SATQBFk, and SATQBF respectively. First of all,
we explain the relationship between logic languages and complexity classes. Then we
give formal definitions and examples for FO (First-Order), SO and
HO (i≥2) (Higher-Order logic). It is known that, for every k ≥1, SATQBFk is a
complete problem for the level Σ [superscript P subscript k] of PH (Polynomial-time hierarchy), and
that SATQBF is a complete problem for PSPACE. As the expressibility of SO is
known to equal the class PH, then we know that there must be an SO formula which
can express SATQBFk. On the other hand, PSPACE is known to be equal in
expressive power to SO with the addition of a second order transitive closure
quantifier, which is widely conjectured to be strictly more expressive than SO alone.
As TO includes PSPACE , this means that there must be a TO formula that can
express SATQBF . Here we give first a top down explanation on the use of SO to
express SATQBFk. A detailed SO formula is presented. We then give a top down
presentation of the sketch of a TO formula for SATQBF.
Description
Keywords
Boolean logic, Satisfiability problem, Computer algorithms, Logic languages