The Library
Higher-order quantified Boolean satisfiability
Tools
Chistikov, Dmitry, Haase, Christoph, Hadizadeh, Zahra and Mansutti, Alessio (2022) Higher-order quantified Boolean satisfiability. In: 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), Vienna, Austria, 22-26 Aug 2022. Published in: Proceedings of the International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), 241 ISBN 9783959772563. doi:10.4230/LIPIcs.MFCS.2022.33 ISSN 1868-8969.
|
PDF
WRAP-Higher-order-quantified-Boolean-satisfiability-Chistikov-2022.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (989Kb) | Preview |
Official URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.33
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 k-NEXP 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 higher-order 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 TOWER-complete, and that HOSAT(k,d) is complete for the weak k-EXP 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 first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic.
Item Type: | Conference Item (Paper) | ||||||
---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics | ||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
Library of Congress Subject Headings (LCSH): | Algebra, Boolean, Algorithms, Logic, Symbolic and mathematical, Computer science -- Mathematics | ||||||
Series Name: | Leibniz International Proceedings in Informatics (LIPIcs) | ||||||
Journal or Publication Title: | Proceedings of the International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) | ||||||
Publisher: | Schloss Dagstuhl — Leibniz-Zentrum für Informatik | ||||||
Place of Publication: | Dagstuhl, Germany | ||||||
ISBN: | 9783959772563 | ||||||
ISSN: | 1868-8969 | ||||||
Official Date: | 22 August 2022 | ||||||
Dates: |
|
||||||
Volume: | 241 | ||||||
Article Number: | 33 | ||||||
DOI: | 10.4230/LIPIcs.MFCS.2022.33 | ||||||
Status: | Peer Reviewed | ||||||
Publication Status: | Published | ||||||
Access rights to Published version: | Open Access (Creative Commons) | ||||||
Date of first compliant deposit: | 23 August 2022 | ||||||
Date of first compliant Open Access: | 23 August 2022 | ||||||
RIOXX Funder/Project Grant: |
|
||||||
Conference Paper Type: | Paper | ||||||
Title of Event: | 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) | ||||||
Type of Event: | Conference | ||||||
Location of Event: | Vienna, Austria | ||||||
Date(s) of Event: | 22-26 Aug 2022 | ||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year