liu.seSök publikationer i DiVA
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Solving Quantified Boolean Formulas with Few Existential Variables
Linköpings universitet, Institutionen för datavetenskap, Artificiell intelligens och integrerade datorsystem. Linköpings universitet, Tekniska fakulteten.
Linköpings universitet, Institutionen för datavetenskap, Artificiell intelligens och integrerade datorsystem. Linköpings universitet, Tekniska fakulteten.
Univ Leeds, England.
Linköpings universitet, Institutionen för datavetenskap, Artificiell intelligens och integrerade datorsystem. Linköpings universitet, Tekniska fakulteten.ORCID-id: 0000-0002-2884-9837
Visa övriga samt affilieringar
2024 (Engelska)Ingår i: PROCEEDINGS OF THE THIRTY-THIRD INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, IJCAI 2024, IJCAI-INT JOINT CONF ARTIF INTELL , 2024, s. 1889-1897Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
IJCAI-INT JOINT CONF ARTIF INTELL , 2024. s. 1889-1897
Nationell ämneskategori
Beräkningsmatematik
Identifikatorer
URN: urn:nbn:se:liu:diva-212053ISI: 001347142802001ISBN: 9781956792041 (tryckt)OAI: oai:DiVA.org:liu-212053DiVA, id: diva2:1942597
Konferens
33rd International Joint Conference on Artificial Intelligence (IJCAI), Jeju, SOUTH KOREA, aug 03-09, 2024
Anmärkning

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

Tillgänglig från: 2025-03-05 Skapad: 2025-03-05 Senast uppdaterad: 2025-09-12
Ingår i avhandling
1. Infinite-Domain CSPs and QBF: Fine-Grained and Parameterized Complexity
Öppna denna publikation i ny flik eller fönster >>Infinite-Domain CSPs and QBF: Fine-Grained and Parameterized Complexity
2025 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
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. 

Ort, förlag, år, upplaga, sidor
Linköping: Linköping University Electronic Press, 2025. s. 27
Serie
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 2471
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:liu:diva-217673 (URN)10.3384/9789181182149 (DOI)9789181182132 (ISBN)9789181182149 (ISBN)
Disputation
2025-10-20, Ada Lovelace, B Building, Campus Valla, Linköping, 13:15 (Engelska)
Opponent
Handledare
Anmärkning

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

Tillgänglig från: 2025-09-12 Skapad: 2025-09-12 Senast uppdaterad: 2025-10-27Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Sök vidare i DiVA

Av författaren/redaktören
Eriksson, LeifLagerkvist, VictorOsipov, George
Av organisationen
Artificiell intelligens och integrerade datorsystemTekniska fakulteten
Beräkningsmatematik

Sök vidare utanför DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 126 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf