Chistikov, Dmitry ;
Haase, Christoph ;
Hadizadeh, Zahra ;
Mansutti, Alessio
HigherOrder Quantified Boolean Satisfiability
Abstract
The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXP. While, in theory, iterating this approach yields complete problems for kNEXP for all k > 0, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds.
The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higherorder Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k,d), k ≥ 0, d ≥ 1, in which variables are interpreted as Boolean functions of order at most k and there are d quantifier alternations between functions of order exactly k. We show that the unbounded HOSAT problem is TOWERcomplete, and that HOSAT(k,d) is complete for the weak kEXP hierarchy with d alternations for fixed k,d ≥ 1 and d odd.
We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the firstorder theory of the integers with addition and equality but without order. It has been a longstanding open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negationfree fragment and the Horn fragment of weak Presburger arithmetic.
BibTeX  Entry
@InProceedings{chistikov_et_al:LIPIcs.MFCS.2022.33,
author = {Chistikov, Dmitry and Haase, Christoph and Hadizadeh, Zahra and Mansutti, Alessio},
title = {{HigherOrder Quantified Boolean Satisfiability}},
booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
pages = {33:133:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772563},
ISSN = {18688969},
year = {2022},
volume = {241},
editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16831},
URN = {urn:nbn:de:0030drops168313},
doi = {10.4230/LIPIcs.MFCS.2022.33},
annote = {Keywords: Boolean satisfiability problem, higherorder Boolean functions, weak kEXP hierarchies, nonelementary complexity, Presburger arithmetic}
}
22.08.2022
Keywords: 

Boolean satisfiability problem, higherorder Boolean functions, weak kEXP hierarchies, nonelementary complexity, Presburger arithmetic 
Seminar: 

47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Issue date: 

2022 
Date of publication: 

22.08.2022 