liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Solving Quantified Boolean Formulas with Few Existential Variables
Linköping University, Department of Computer and Information Science, Artificial Intelligence and Integrated Computer Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Artificial Intelligence and Integrated Computer Systems. Linköping University, Faculty of Science & Engineering.
Univ Leeds, England.
Linköping University, Department of Computer and Information Science, Artificial Intelligence and Integrated Computer Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0002-2884-9837
Show others and affiliations
2024 (English)In: PROCEEDINGS OF THE THIRTY-THIRD INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, IJCAI 2024, IJCAI-INT JOINT CONF ARTIF INTELL , 2024, p. 1889-1897Conference paper, Published paper (Refereed)
Abstract [en]

The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state of the art SAT solvers, which has prevented QBF from becoming a universal modelling language for PSPACE-complete problems. A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters guaranteeing fixed-parameter tractability (FPT). In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. This natural parameter is virtually unexplored in the literature which one might find surprising given the general scarcity of FPT algorithms for QBF. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis.

Place, publisher, year, edition, pages
IJCAI-INT JOINT CONF ARTIF INTELL , 2024. p. 1889-1897
National Category
Computational Mathematics
Identifiers
URN: urn:nbn:se:liu:diva-212053ISI: 001347142802001ISBN: 9781956792041 (print)OAI: oai:DiVA.org:liu-212053DiVA, id: diva2:1942597
Conference
33rd International Joint Conference on Artificial Intelligence (IJCAI), Jeju, SOUTH KOREA, aug 03-09, 2024
Note

Funding Agencies|Swedish research council [VR-2022-03214]; Wallenberg AI, Autonomous Systems and Software Program (WASP) - Knut and Alice Wallenberg Foundation

Available from: 2025-03-05 Created: 2025-03-05 Last updated: 2025-09-12
In thesis
1. Infinite-Domain CSPs and QBF: Fine-Grained and Parameterized Complexity
Open this publication in new window or tab >>Infinite-Domain CSPs and QBF: Fine-Grained and Parameterized Complexity
2025 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

While we today have quite powerful tools for solving problems that are NP-hard, or even harder ones, it is typically easy to give conditions where they exhibit impractical slow performance. When designing new, better, algorithms for these cases, understanding theoretical limits becomes crucial to avoid investing time in approaches that are ultimately dead ends. Modern conjectures, such as the exponential time hypothesis (ETH), enable us to establish effective theoretical lower bounds for many problems. These lower bounds often align closely with our best-known upper bounds, especially in problems over finite domains. However, this alignment tends to break down in cases involving infinite domains, or input-dependent domains, and for problems beyond NP. While we for some easier and harder infinite-domain problems have matching upper and lower bounds, there exists a wide range of problems where a significant knowledge gap remains. We specifically examine Allen’s interval algebra (Allen) and partially ordered time (POT), where the best known lower bounds are 2o(n). Both these problems can be formulated as infinite-domain constraint satisfaction problems (CSP) and exhibit this gap between upper and lower bounds. While these problems are solvable in 2O(n2) time by exhaustive search, we improve upon this and ultimately reach the first o(n)n algorithm for Allen. This result is the usage of dynamic programming, with a particular emphasis on tracking unsolved subproblems, rather than the more traditional approach of building upon already-solved subproblems.

While a significant improvement over exhaustive search, to get closer to single-exponential running times of 2O(n2), we shift our focus to (multivariate) parameterized complexity. We begin by introducing two new single-exponential complexity classes: fixed parameter single-exponential (FPE) and slicewise single-exponential (XE), analogous to the well-known classes of fixed-parameter tractable (FPT) and slicewise polynomial (XP), respectively. We then apply these concepts to Allen and POT, showing both FPE and XE results.

In the latter part of the thesis we shift focus to a problem where further unconditional improvements are unlikely under the strong ETH: evaluating quantified Boolean formulas (QBF). Although this problem is the PSpace-complete analogue of the Boolean Satisfiability problem (SAT), it is comparatively understudied, and few positive algorithmic results are known. Focusing on how simplifying away a small set of variables (a backdoor) results in a tractable formula, we start by showing how removing all existential variables yields new FPT results. Building upon this, we then show multiple other backdoor results for classical tractable classes like 2-CNF, AFF and HORN, including both new hardness results and new FPT algorithms. 

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 2025. p. 27
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 2471
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-217673 (URN)10.3384/9789181182149 (DOI)9789181182132 (ISBN)9789181182149 (ISBN)
Public defence
2025-10-20, Ada Lovelace, B Building, Campus Valla, Linköping, 13:15 (English)
Opponent
Supervisors
Note

Funding agency: The National Graduate School of Computer Science in Sweden (CUGS)

Available from: 2025-09-12 Created: 2025-09-12 Last updated: 2025-10-27Bibliographically approved

Open Access in DiVA

No full text in DiVA

Search in DiVA

By author/editor
Eriksson, LeifLagerkvist, VictorOsipov, George
By organisation
Artificial Intelligence and Integrated Computer SystemsFaculty of Science & Engineering
Computational Mathematics

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 118 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf