Leif Eriksson

Leif Eriksson, Victor Lagerkvist, Sebastian Ordyniak et al.

The quantified Boolean formula problem (QBF) is a well-known PSpace-complete problem with rich expressive power, and is generally viewed as the SAT analogue for PSpace. Given that many problems today are solved in practice by reducing to SAT, and then using highly optimized SAT solvers, it is natural to ask whether problems in PSpace are amenable to this approach. While SAT solvers exploit hidden structural properties, such as backdoors to tractability, backdoor analysis for QBF is comparatively very limited. We present a comprehensive study of the (parameterized) complexity of QBF parameterized by backdoor size to the largest tractable syntactic classes: HORN, 2-SAT, and AFFINE. While SAT is in FPT under this parameterization, we prove that QBF remains PSpace-hard even on formulas with backdoors of constant size. Parameterizing additionally by the quantifier depth, we design FPT-algorithms for the classes 2-SAT and AFFINE, and show that 3-HORN is W[1]-hard. As our next contribution, we vastly extend the applicability of QBF backdoors not only for the syntactic classes defined above but also for tractable classes defined via structural restrictions, such as formulas with bounded incidence treewidth and quantifier depth. To this end, we introduce enhanced backdoors: these are separators S of size at most k in the primal graph such that S together with all variables contained in any purely universal component of the primal graph minus S is a backdoor. We design FPT-algorithms with respect to k for both evaluation and detection of enhanced backdoors to all tractable classes of QBF listed above and more.

Victor Lagerkvist, Johanna Groven, Leif Eriksson

The region connection calculus ($RCC$) and Allen's interval algebra ($IA$) are two well-known NP-hard spatial-temporal qualitative reasoning problems. They are solvable in $2^{O(n \log n)}$ time, where $n$ is the number of variables, and $IA$ is additionally known to be solvable in $o(n)^n$ time. However, no improvement over exhaustive search is known for $RCC$, and if they are also solvable in single exponential time $2^{O(n)}$ is unknown. We investigate multiple avenues towards reaching such bounds. First, we show that branching is insufficient since there are too many non-redundant constraints. Concretely, we classify the maximum number of non-redundant constraints in $RCC$ and $IA$. Algorithmically, we make two significant contributions based on dynamic programming (DP). The first algorithm runs in $4^n$ time and is applicable to a non-trivial, NP-hard fragment of $IA$, which includes the well-known interval graph sandwich problem of Golumbic and Shamir (1993). For the richer $RCC$ problem with 8 basic relations we use a more sophisticated approach which asymptotically matches the $o(n)^n$ bound for $IA$.

Leif Eriksson, Victor Lagerkvist

Qualitative reasoning is an important subfield of artificial intelligence where one describes relationships with qualitative, rather than numerical, relations. Many such reasoning tasks, e.g., Allen's interval algebra, can be solved in $2^{O(n \cdot \log n)}$ time, but single-exponential running times $2^{O(n)}$ are currently far out of reach. In this paper we consider single-exponential algorithms via a multivariate analysis consisting of a fine-grained parameter $n$ (e.g., the number of variables) and a coarse-grained parameter $k$ expected to be relatively small. We introduce the classes FPE and XE of problems solvable in $f(k) \cdot 2^{O(n)}$, respectively $f(k)^n$, time, and prove several fundamental properties of these classes. We proceed by studying temporal reasoning problems and (1) show that the Partially Ordered Time problem of effective width $k$ is solvable in $16^{kn}$ time and is thus included in XE, and (2) that the network consistency problem for Allen's interval algebra with no interval overlapping with more than $k$ others is solvable in $(2nk)^{2k} \cdot 2^{n}$ time and is included in FPE. Our multivariate approach is in no way limited to these to specific problems and may be a generally useful approach for obtaining single-exponential algorithms.

Leif Eriksson, Victor Lagerkvist, Sebastian Ordyniak et al.

Determining the validity of a quantified Boolean formula (QBF) is a PSPACE-complete problem with rich expressive power. Despite interest in efficient solvers, there is, compared to problems in NP, a lack of positive theoretical results, and in the parameterized complexity setting one often has to restrict the quantifier prefix (e.g., bounding alternations) to obtain fixed parameter tractability (FPT). We propose a new parameter: the number of variables in clauses that has to be removed before reaching a tractable class (a clause covering (CC) backdoor). We are then interested in solving QBF in FPT time given a CC-backdoor of size $k$. We consider the three classical, tractable cases of QBF as base classes: Horn, 2-CNF, and linear equations. We establish W[1]-hardness for Horn but prove FPT for the others, and prove that in a precise, algebraic sense, we are only missing one important case for a full dichotomy. Our algorithms are non-trivial and depend on propagation, and Gaussian elimination, respectively, and are comparably unexplored for QBF.

Leif Eriksson, Victor Lagerkvist, George Osipov et al.

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.

Leif Eriksson, Victor Lagerkvist

Allen's interval algebra is one of the most well-known calculi in qualitative temporal reasoning with numerous applications in artificial intelligence. Recently, there has been a surge of improvements in the fine-grained complexity of NP-hard reasoning tasks, improving the running time from the naive $2^{O(n^2)}$ to $O^*((1.0615n)^{n})$, with even faster algorithms for unit intervals a bounded number of overlapping intervals (the $O^*(\cdot)$ notation suppresses polynomial factors). Despite these improvements the best known lower bound is still only $2^{o(n)}$ (under the exponential-time hypothesis) and major improvements in either direction seemingly require fundamental advances in computational complexity. In this paper we propose a novel framework for solving NP-hard qualitative reasoning problems which we refer to as dynamic programming with sublinear partitioning. Using this technique we obtain a major improvement of $O^*((\frac{cn}{\log{n}})^{n})$ for Allen's interval algebra. To demonstrate that the technique is applicable to more domains we apply it to a problem in qualitative spatial reasoning, the cardinal direction point algebra, and solve it in $O^*((\frac{cn}{\log{n}})^{2n/3})$ time. Hence, not only do we significantly advance the state-of-the-art for NP-hard qualitative reasoning problems, but obtain a novel algorithmic technique that is likely applicable to many problems where $2^{O(n)}$ time algorithms are unlikely.

Leif Eriksson, Victor Lagerkvist

Partially ordered models of time occur naturally in applications where agents or processes cannot perfectly communicate with each other, and can be traced back to the seminal work of Lamport. In this paper we consider the problem of deciding if a (likely incomplete) description of a system of events is consistent, the network consistency problem for the point algebra of partially ordered time (POT). While the classical complexity of this problem has been fully settled, comparably little is known of the fine-grained complexity of POT except that it can be solved in $O^*((0.368n)^n)$ time by enumerating ordered partitions. We construct a much faster algorithm with a run-time bounded by $O^*((0.26n)^n)$. This is achieved by a sophisticated enumeration of structures similar to total orders, which are then greedily expanded toward a solution. While similar ideas have been explored earlier for related problems it turns out that the analysis for POT is non-trivial and requires significant new ideas.