Answer Set Programming (ASP) is a mature and widely used framework for modeling and solving problems in AI, knowledge representation and reasoning, and combinatorial search. Counting answer sets is of growing importance for analyzing search spaces, navigating ASP programs, and enabling probabilistic reasoning. While Truszczynski established a complete hierarchy for the computational complexity of ASP decision and reasoning problems (skeptical and credulous), a corresponding systematic treatment of counting problems has been missing so far. We close this gap by providing an almost complete characterisation of the counting complexity landscape for ASP. A remaining gap arises between Krom and Horn programs, caused by the minimality of disjunctions in Krom rule heads for guessing. To address this issue, we replace disjunctions with choice rules and introduce a controlled fragment in which choices are allowed and every rule is simultaneously Horn and Krom (Choice-Horn-Krom). We show that this fragment does not admit an polynomial-time approximation scheme (FPRAS) under standard complexity-theoretic assumptions. However, we prove that counting answer sets of an arbitrary ASP program can already be done by counting answer sets of two Choice-Horn-Krom programs. This result demonstrates the expressive power of ASP and yields a conceptually simpler alternative to Valiant's classical reduction from #SAT to #Krom-SAT, which a very well-known result in propositional logic.

This document contains a short description of our solver for the dominating set and hitting set problems that we submitted to the exact tracks of the PACE Challenge 2025. The solver is based on a straightforward MaxSAT formulation supplemented by hitting-set-based reduction rules. It utilizes a clique solver if the reduced instance is a (small) input for the vertex cover problem and tries to match certain lower bounds by expressing the reduced instance as a sat problem.

Model counting is a powerful extension of constraint reasoning that, instead of finding a solution to a constraint system, allows to identify the number of such solutions. Cardinality constraints are used to filter solutions of a certain quality by restricting the number of elements that can be added to the solution. Naturally, one would like to combine both in order to count the number of solutions of good quality. Unfortunately, the two concepts do not get along so well as (1) cardinality constraints may not be parsimonious (due to auxiliary variables, the system’s number of solutions may change in an uncontrolled way) and (2) such constraints may destroy structural properties, which are crucial for the performance of modern solvers. This article provides a systematic study of existing cardinality constraints in the light of model counting, observing that none of them are both, parsimonious and treewidth-preserving. We present structure-aware cardinality constraints that are parsimonious and guaranteed to increase the input’s treewidth only in a controlled way. Detailed experiments reveal that our encodings outperform existing ones.

The canonical class in the realm of counting complexity is #P. It is well known that the problem of counting the models of a propositional formula in disjunctive normal form (#DNF) is complete for #P under Turing reductions. On the other hand, #DNF ∈ spanL and spanL ⊋ #P unless#DNFNL = NPis a strict. Hence, the class of functions logspace-reducible to subset of #P under plausible complexity-theoretic assumptions. By contrast, we show that two calls to a (restricted) #2DNF oracle suffice to capture gapP, namely, that the logspace many-one closure of the subtraction between the results of two #2DNF calls is gapP. Because #P ⊋ gapP, #P is strictly contained between one and two #2DNF oracle calls.Surprisingly, the propositional formulas needed in both calls are linear-time computable, and the reduction preserves interesting structural as well as symmetry properties, leading to algorithmic applications. We show that a single subtraction suffices to compensate for the absence of negation while still capturing gapP, i.e., our results carry over to the monotone fragments of #2SAT and #2DNF. Since our reduction is linear-time, it preserves sparsity and, as a consequence we obtain a sparsification lemma for both #2SAT and #2DNF. This has only been known for kSAT with k ≥ 3 and respective counting versions.We further show that both single call if we allow a little postprocessing (computable by AC0-or TC0-circuits). Consequently, we derive refined versions of Toda’s Theorem: ${\text{PH}} \subseteq [\# {\text{MON}}2{\text{SAT}}]_{{\text{T}}{{\text{C}}^0}}^{\log } = [\# {\text{MON}}2{\text{DNF}}]_{{\text{T}}{{\text{C}}^0}}^{\log }$. Our route to these results is via structure-aware reductions that preserve parameters like treewidth up to an additive overhead. The absence of multiplicative overhead indeed yields parameterized SETH-tight lower bounds.

Algorithmic meta-theorems state that problems definable in a fixed logic can be solved efficiently on structures with certain properties. An example is Courcelle’s Theorem, which states that all problems expressible in monadic second-order logic can be solved efficiently on structures of small treewidth. Such theorems are usually proven by algorithms for the model-checking problem of the logic, which is often complex and rarely leads to highly efficient solutions. Alternatively, we can solve the model-checking problem by grounding the given logic to propositional logic, for which dedicated solvers are available. Such encodings will, however, usually not preserve the input’s treewidth. This paper investigates whether all problems definable in monadic second-order logic can efficiently be encoded into SAT such that the input’s treewidth bounds the treewidth of the resulting formula. We answer this in the affirmative and, hence, provide an alternative proof of Courcelle’s Theorem. Our technique can naturally be extended: There are treewidth-aware reductions from the optimization version of Courcelle’s Theorem to MAXSAT and from the counting version of the theorem to #SAT. By using encodings to SAT, we obtain, ignoring polynomial factors, the same running time for the model-checking problem as we would with dedicated algorithms. Another immediate consequence is a treewidth-preserving reduction from the model-checking problem of monadic second-order logic to integer linear programming (ILP). We complement our upper bounds with new lower bounds based on ETH; and we show that the block size of the input’s formula and the treewidth of the input’s structure are tightly linked. Finally, we present various side results needed to prove the main theorems: A treewidth-preserving cardinality constraints, treewidth-preserving encodings from CNFs into DNFs, and a treewidth-aware quantifier elimination scheme for QBF implying a treewidth-preserving reduction from QSAT to SAT. We also present a reduction from projected model counting to #SAT that increases the treewidth by at most a factor of 2^{k+3.59}, yielding a algorithm for projected model counting that beats the currently best running time of 2^{2^{k+4}}⋅poly(|ψ|).

Maximum model counting$(\text{MAX}\#\exists \text{SAT})$is a recently introduced extension of projected model counting$(\#\exists \text{SAT})$that maximizes over a set of variables$X$the number of assignments over a set$Y$that can be extended to a satisfying assignment over$Z$. It is known that$\text{MAX}\#\exists \text{SAT}$also generalizes weighted$\#\exists \text{SAT}$and MAXSAT if weights are introduced to the problem. However, for the latter a non-trivial gadget is needed. We propose a more generic weighting scheme that evaluates a fitness term and a probability term simultaneously. In this setting,$\text{MAX}\#\exists \text{SAT}$extends weighted MAXSAT and$\#\exists \text{SAT}$without the need of gadgets. As MAXSAT is the canonical problem of cost-optimal reasoning and$\#\exists \text{SAT}$can be seen as canonical problem of probabilistic reasoning,$\text{MAX}\# 3\text{SAT}$with the proposed weighting scheme naturally fills the role as canonical problem for cost-optimal probabilistic reasoning. We study the problem from a complexity-theoretic point of view for unary weights and prove that the decision version is$\mathrm{D}_{2}^{\mathrm{P}}{-}$complete. We then focus on structural parameters and provide an ETH lower bound with respect to the inputs treewidth, as well as a treewidth-aware reduction from$\text{MAX}\#\exists \text{SAT}$to$\text{MAX}\#\exists \text{SAT}$.

Vertex deletion problems for graphs are studied intensely in classical and parameterized complexity theory. They ask whether we can delete at most k vertices from an input graph such that the resulting graph has a certain property. Regarding k as the parameter, a dichotomy was recently shown based on the number of quantifier alternations of first-order formulas that describe the property. In this paper, we refine this classification by moving from quantifier alternations to individual quantifier patterns and from a dichotomy to a trichotomy, resulting in a complete classification of the complexity of vertex deletion problems based on their quantifier pattern. The more fine-grained approach uncovers new tractable fragments, which we show to not only lie in FPT, but even in parameterized constant-depth circuit complexity classes. On the other hand, we show that vertex deletion becomes intractable already for just one quantifier per alternation, that is, there is a formula of the form {\forall}x{\exists}y{\forall}z(ψ), with ψ quantifier-free, for which the vertex deletion problem is W[1]-hard. The fine-grained analysis also allows us to uncover differences in the complexity landscape when we consider different kinds of graphs and more general structures: While basic graphs (undirected graphs without self-loops), undirected graphs, and directed graphs each have a different frontier of tractability, the frontier for arbitrary logical structures coincides with that of directed graphs.

Enumerating the directed acyclic graphs (DAGs) of a Markov equivalence class (MEC) is an important primitive in causal analysis. The central resource from the perspective of computational complexity is the delay, that is, the time an algorithm that lists all members of the class requires between two consecutive outputs. Commonly used algorithms for this task utilize the rules proposed by Meek (1995) or the transformational characterization by Chickering (1995), both resulting in superlinear delay. In this paper, we present the first linear-time delay algorithm. On the theoretical side, we show that our algorithm can be generalized to enumerate DAGs represented by models that incorporate background knowledge, such as MPDAGs; on the practical side, we provide an efficient implementation and evaluate it in a series of experiments. Complementary to the linear-time delay algorithm, we also provide intriguing insights into Markov equivalence itself: All members of an MEC can be enumerated such that two successive DAGs have structural Hamming distance at most three.

By Fagin's Theorem, NP contains precisely those problems that can be described by formulas starting with an existential second-order quantifier, followed by only first-order quantifiers (ESO formulas). Subsequent research refined this result, culminating in powerful theorems that characterize for each possible sequence of first-order quantifiers how difficult the described problem can be. We transfer this line of inquiry to the parameterized setting, where the size of the set quantified by the second-order quantifier is the parameter. Many natural parameterized problems can be described in this way using simple sequences of first-order quantifiers: For the clique or vertex cover problems, two universal first-order quantifiers suffice ("for all pairs of vertices ... must hold"); for the dominating set problem, a universal followed by an existential quantifier suffice ("for all vertices, there is a vertex such that ..."); and so on. We present a complete characterization that states for each possible sequence of first-order quantifiers how high the parameterized complexity of the described problems can be. The uncovered dividing line between quantifier sequences that lead to tractable versus intractable problems is distinct from that known from the classical setting, and it depends on whether the parameter is a lower bound on, an upper bound on, or equal to the size of the quantified set.

In the maximum satisfiability problem (max-sat) we are given a propositional formula in conjunctive normal form and have to find an assignment that satisfies as many clauses as possible. We study the parallel parameterized complexity of various versions of max-sat and provide the first constant-time algorithms parameterized either by the solution size or by the allowed excess relative to some guarantee. For the dual parameterized version where the parameter is the number of clauses we are allowed to leave unsatisfied, we present the first parallel algorithm for max-2sat (known as almost-2sat). The difficulty in solving almost-2sat in parallel comes from the fact that the iterative compression method, originally developed to prove that the problem is fixed-parameter tractable at all, is inherently sequential. We observe that a graph flow whose value is a parameter can be computed in parallel and develop a parallel algorithm for the vertex cover problem parameterized above the size of a given matching. Finally, we study the parallel complexity of max-sat parameterized by the vertex cover number, the treedepth, the feedback vertex set number, and the treewidth of the input’s incidence graph. While max-sat is fixedparameter tractable for all of these parameters, we show that they allow different degrees of possible parallelization. For all four we develop dedicated parallel algorithms that are constructive, meaning that they output an optimal assignment – in contrast to results that can be obtained by parallel meta-theorems, which often only solve the decision version.

Counting and sampling directed acyclic graphs from a Markov equivalence class are fundamental tasks in graphical causal analysis. In this paper we show that these tasks can be performed in polynomial time, solving a long-standing open problem in this area. Our algorithms are effective and easily implementable. As we show in experiments, these breakthroughs make thought-to-be-infeasible strategies in active learning of causal structures and causal effect identification with regard to a Markov equivalence class practically applicable.

In the maximum satisfiability problem (MAX-SAT) we are given a propositional formula in conjunctive normal form and have to find an assignment that satisfies as many clauses as possible. We study the parallel parameterized complexity of various versions of MAX-SAT and provide the first constant-time algorithms parameterized either by the solution size or by the allowed excess relative to some guarantee ("above guarantee" versions). For the dual parameterized version where the parameter is the number of clauses we are allowed to leave unsatisfied, we present the first parallel algorithm for MAX-2SAT (known as ALMOST-2SAT). The difficulty in solving ALMOST-2SAT in parallel comes from the fact that the iterative compression method, originally developed to prove that the problem is fixed-parameter tractable at all, is inherently sequential. We observe that a graph flow whose value is a parameter can be computed in parallel and use this fact to develop a parallel algorithm for the vertex cover problem parameterized above the size of a given matching. Finally, we study the parallel complexity of MAX-SAT parameterized by the vertex cover number, the treedepth, the feedback vertex set number, and the treewidth of the input's incidence graph. While MAX-SAT is fixed-parameter tractable for all of these parameters, we show that they allow different degrees of possible parallelization. For all four we develop dedicated parallel algorithms that are constructive, meaning that they output an optimal assignment - in contrast to results that can be obtained by parallel meta-theorems, which often only solve the decision version.

Ancestral graphs are an important tool for encoding causal knowledge as they represent uncertainty about the presence of latent confounding and selection bias, and they can be inferred from data. As for other graphical models, several maximal ancestral graphs (MAGs) may encode the same statistical information in the form of conditional independencies. Such MAGs are said to be Markov equivalent. This work concerns graphical characterizations and computational aspects of Markov equivalence between MAGs. These issues have been studied in past years leading to several criteria and methods to test Markov equivalence. The state-of-the-art algorithm, provided by Hu and Evans [UAI 2020], runs in time $O(n^5)$ for instances with $n$ vertices. We propose a new constructive graphical criterion for the Markov equivalence of MAGs, which allows us to develop a practically effective equivalence test with worst-case runtime $O(n^3)$. Additionally, our criterion is expressed in terms of natural graphical concepts, which is of independent value.

Abstract Computing small kernels for the hitting set problem is a well-studied computational problem where we are given a hypergraph with n vertices and m hyperedges, each of size d for some small constant d, and a parameter k. The task is to compute a new hypergraph, called a kernel, whose size is polynomial with respect to the parameter k and which has a size-k hitting set if, and only if, the original hypergraph has one. State-of-the-art algorithms compute kernels of size $$k^d$$ k d (which is a polynomial as d is a constant), and they do so in time $$m\cdot 2^d {\text {poly}}(d)$$ m · 2 d poly ( d ) for a small polynomial $${\text {poly}}(d)$$ poly ( d ) (which is linear in the hypergraph size for d fixed). We generalize this task to the dynamic setting where hyperedges may continuously be added or deleted and one constantly has to keep track of a size- $$k^d$$ k d kernel. This paper presents a deterministic solution with worst-case time $$3^d {\text {poly}}(d)$$ 3 d poly ( d ) for updating the kernel upon inserts and time $$5^d {\text {poly}}(d)$$ 5 d poly ( d ) for updates upon deletions. These bounds nearly match the time $$2^d {\text {poly}}(d)$$ 2 d poly ( d ) needed by the best static algorithm per hyperedge. Let us stress that for constant d our algorithm maintains a hitting set kernel with constant, deterministic, worst-case update time that is independent of n, m, and the parameter k. As a consequence, we also get a deterministic dynamic algorithm for keeping track of size-k hitting sets in d-hypergraphs with update times O(1) and query times $$O(c^k)$$ O ( c k ) where $$c = d - 1 + O(1/d)$$ c = d - 1 + O ( 1 / d ) equals the best base known for the static setting.

Counting and uniform sampling of directed acyclic graphs (DAGs) from a Markov equivalence class are fundamental tasks in graphical causal analysis. In this paper, we show that these tasks can be performed in polynomial time, solving a long-standing open problem in this area. Our algorithms are effective and easily implementable. Experimental results show that the algorithms significantly outperform state-of-the-art methods.

Computing small kernels for the hitting set problem is a well-studied computational problem where we are given a hypergraph with n vertices and m hyperedges, each of size d for some small constant d, and a parameter k. The task is to compute a new hypergraph, called a kernel, whose size is polynomial with respect to the parameter k and which has a size-k hitting set if, and only if, the original hypergraph has one. State-of-the-art algorithms compute kernels of size k^d (which is a polynomial kernel size as d is a constant), and they do so in time m⋅ 2^d poly(d) for a small polynomial poly(d) (which is a linear runtime as d is again a constant). We generalize this task to the dynamic setting where hyperedges may continuously be added or deleted and one constantly has to keep track of a size-k^d hitting set kernel in memory (including moments when no size-k hitting set exists). This paper presents a deterministic solution with worst-case time 3^d poly(d) for updating the kernel upon hyperedge inserts and time 5^d poly(d) for updates upon deletions. These bounds nearly match the time 2^d poly(d) needed by the best static algorithm per hyperedge. Let us stress that for constant d our algorithm maintains a dynamic hitting set kernel with constant, deterministic, worst-case update time that is independent of n, m, and the parameter k. As a consequence, we also get a deterministic dynamic algorithm for keeping track of size-k hitting sets in d-hypergraphs with update times O(1) and query times O(c^k) where c = d - 1 + O(1/d) equals the best base known for the static setting.

Finding a consistent DAG extension for a given partially directed acyclic graph (PDAG) is a basic building block used in graphical causal analysis. In 1992, Dor and Tarsi proposed an algorithm with time complexity O(n^4), which has been widely used in causal theory and practice so far. It is a long-standing open question whether an extension can be computed faster and, in particular, it was conjectured that a linear-time method may exist. The main contributions of our work are two-fold: Firstly, we propose a new algorithm for the extension problem for PDAGs which runs in time O(n^3); secondly, we show that, under a computational intractability assumption, our cubic algorithm is optimal. Thus, our impossibility result disproves the conjecture that a linear-time method exists. Based on these results, we present a full complexity landscape for finding extensions in various causal graphical models. We extend the techniques to recognition problems and apply them to design an effective algorithm for closing a PDAG under the orientation rules of Meek.

Gene order evolution of unichromosomal genomes, for example mitochondrial genomes, has been modelled mostly by four major types of genome rearrangements: inversions, transpositions, inverse transpositions, and tandem duplication random losses. Generalizing models that include all those rearrangements while admitting computational tractability are rare. In this paper, we study such a rearrangement model, namely the inverse tandem duplication random loss (iTDRL) model, where an iTDRL duplicates and inverts a continuous segment of a gene order followed by the random loss of one of the redundant copies of each gene. The iTDRL rearrangement has currently been proposed by several authors suggesting it to be a possible mechanisms of mitochondrial gene order evolution. We initiate the algorithmic study of this new model of genome rearrangement by proving that a shortest rearrangement scenario that transforms one given gene order into another given gene order can be obtained in quasilinear time. Furthermore, we show that the length of such a scenario, i.e., the minimum number of iTDRLs in the transformation, can be computed in linear time.

This document describes the heuristic for computing treedepth decompositions of undirected graphs used by our solve fluid. The heuristic runs four different strategies to find a solution and finally outputs the best solution obtained by any of them. Two strategies are score-based and iteratively remove the vertex with the best score. The other two strategies iteratively search for vertex separators and remove them. We also present implementation strategies and data structures that significantly improve the run time complexity and might be interesting on their own.

This document provides a short overview of our treedepth solver PID^{⋆} in the version that we submitted to the exact track of the PACE challenge 2020. The solver relies on the positive-instance driven dynamic programming (PID) paradigm that was discovered in the light of earlier iterations of the PACE in the context of treewidth. It was recently shown that PID can be used to solve a general class of vertex pursuit-evasion games - which include the game theoretic characterization of treedepth. Our solver PID^{⋆} is build on top of this characterization.

Given a hypergraph H = ( V , E ), what is the smallest subset \(X \subseteq V\) such that e ∩ X ≠ ∅ holds for all e ∈ E ? This problem, known as the hitting set problem, is a basic problem in combinatorial optimization and has been studied extensively in both classical and parameterized complexity theory. There are well-known kernelization algorithms for it, which get a hypergraph H and a number k as input and output a hypergraph H ′ such that (1) H has a hitting set of size k if and only if \(H^{\prime }\) has such a hitting set and (2) the size of \(H^{\prime }\) depends only on k and on the maximum cardinality d of hyperedges in H . The algorithms run in polynomial time and can be parallelized to a certain degree: one can easily compute hitting set kernels in parallel time O ( k ) and not-so-easily in time O ( d ) – but it was conjectured that these are the best parallel algorithms possible. We refute this conjecture and show how hitting set kernels can be computed in constant parallel time. For our proof, we introduce a new, generalized notion of hypergraph sunflowers and show how iterated applications of the color coding technique can sometimes be collapsed into a single application.

Parallel fixed-parameter tractability studies how parameterized problems can be solved in parallel. A surprisingly large number of parameterized problems admit a high level of parallelization, but this does not mean that we can also efficiently compute small problem kernels in parallel: known kernelization algorithms are typically highly sequential. In the present paper, we establish a number of upper and lower bounds concerning the sizes of kernels that can be computed in parallel. An intriguing finding is that there are complex trade-offs between kernel size and the depth of the circuits needed to compute them: For the vertex cover problem, an exponential kernel can be computed by AC$^0$-circuits, a quadratic kernel by TC$^0$-circuits, and a linear kernel by randomized NC-circuits with derandomization being possible only if it is also possible for the matching problem. Other natural problems for which similar (but quantitatively different) effects can be observed include tree decomposition problems parameterized by the vertex cover number, the undirected feedback vertex set problem, the matching problem, or the point line cover problem. We also present natural problems for which computing kernels is inherently sequential.

While the theoretical aspects concerning the computation of tree width - one of the most important graph parameters - are well understood, it is not clear how it can be computed practically. We present the open source Java library Jdrasil that implements several different state of the art algorithms for this task. By experimentally comparing these algorithms, we show that the default choices made in Jdrasil lead to an competitive implementation (it took the third place in the first PACE challenge) while also being easy to use and easy to extend.

Algorithmic meta-theorems are general algorithmic results applying to a whole range of problems, rather than just to a single problem alone. They often have a "logical" and a "structural" component, that is they are results of the form: every computational problem that can be formalised in a given logic L can be solved efficiently on every class C of structures satisfying certain conditions. This paper gives a survey of algorithmic meta-theorems obtained in recent years and the methods used to prove them. As many meta-theorems use results from graph minor theory, we give a brief introduction to the theory developed by Robertson and Seymour for their proof of the graph minor theorem and state the main algorithmic consequences of this theory as far as they are needed in the theory of algorithmic meta-theorems.

Fixed-parameter algorithms have been successfully applied to solve numerous difficult problems within acceptable time bounds on large inputs. However, most fixed-parameter algorithms are inherently sequential and, thus, make no use of the parallel hardware present in modern computers. We show that parallel fixed-parameter algorithms do not only exist for numerous parameterized problems from the literature - including vertex cover, packing problems, cluster editing, cutting vertices, finding embeddings, or finding matchings - but that there are parallel algorithms working in constant time or at least in time depending only on the parameter (and not on the size of the input) for these problems. Phrased in terms of complexity classes, we place numerous natural parameterized problems in parameterized versions of AC^0. On a more technical level, we show how the color coding method can be implemented in constant time and apply it to embedding problems for graphs of bounded tree-width or tree-depth and to model checking first-order formulas in graphs of bounded degree.