Work

Abstract: Strategy extraction in QBF proof systems usually attempts to extract winning strategies from valid proofs. However, an alternative (and arguably more powerful) view is to extract Skolem/Herbrand functions, or equivalently synthesis of the game values at all intermediate points. In this paper, we investigate the existence and properties of such proof systems from which one can extract Skolem and Herbrand functions. We propose such a proof system for QBF, which we show is sound and complete, and from which  extraction of Skolem/Herbrand functions can be performed, and game values computed, in polynomial time.

Abstract: Quantified Integer Programming (QIP) bridges multiple domains by extending Quantified Boolean Formulas (QBF) to incorporate general integer variables and linear constraints while also generalizing Integer Programming through variable quantification. Additionally, the inclusion of a linear objective function enables QIP to effectively model multistage robust discrete linear optimization problems, making it a powerful tool for tackling uncertainty in optimization.
While two primary solution paradigms exist for QBF (search-based and expansion-based approaches) only search-based methods have been explored for QIP. We present an expansion-based approach for QIP using Counterexample-Guided Abstraction Refinement (CEGAR), adapting techniques from QBF. We extend this methodology to tackle multistage robust discrete optimization problems with linear constraints and further embed it in an optimization framework, enhancing its applicability.

Abstract: The Ideal Membership Problem (IMP) asks whether a polynomial belongs to a given ideal. While intractable in general, the degree-bounded version IMPd, where the proof of membership is required to have degree at most d, can be solved in n^O(d) arithmetic operations. When the generators arise from constraint satisfaction problems over a constraint language L, the resulting problem IMPd(L) admits a complexity classification in terms of the algebraic structure of operations invariant for L. The degree-bounded IMP is intimately connected to the Polynomial Calculus (PC) proof system, which certifies ideal membership through a sequence of algebraic inferences from the generators. Requiring that the certificate be an explicit PC derivation, rather than allowing any algorithm to decide membership, yields the problem PC-IMPd(L). This is strictly harder than classical IMPd(L) for certain constraint languages, notably those closed under affine operations. Moreover, PC-IMP plays a key role in the degree automatability of Sum-of-Squares (SoS) proofs. It has recently been shown that the bit-complexity barriers currently hindering SoS automatability--low-degree SoS proofs may require exponentially large coefficients, obstructing efficient computation via semidefinite programming--can be overcome whenever the underlying PC-IMP instance is tractable, effectively reducing the SoS automatability question to the study of PC-IMP.
In this work, we develop an algebraic reduction framework for PC-IMP using pp-definitions and pp-encodings, mirroring the polymorphism approach to CSP complexity. As applications, we prove tractability for symmetric majority-closed languages over finite domains via Boolean embedding. Further, we show that degree-d PC proofs from 3Lin(2) axioms have polynomial bit-complexity, meaning that for this language the obstacle to degree automatability lies entirely in degree lower bounds, not in coefficient explosion.

Abstract: Several proof systems for model counting have been introduced in recent years, mainly in an attempt to model #SAT solving and to allow proof logging of solvers. We reexamine these different approaches and show that:
(i) with moderate adaptations, the conceptually quite different proof models of the dynamic system MICE and the static system of annotated Decision-DNNFs are equivalent and
(ii) they tightly characterise state-of-the-art #SAT solving. Thus, these proof systems provide a precise and robust proof-theoretic underpinning of current model counting.
We also propose new strengthenings of these proof systems that might lead to stronger model counters.

Abstract: Sentential Decision Diagrams (SDDs) are data structures, which can succinctly represent many Boolean functions, while still having certain nice algorithmic properties, such as polynomial-time satisfiability checking. Moreover, SDDs are exponentially more succinct than Ordered Binary Decision Diagrams (OBDDs).
Atserias, Kolaitis, and Vardi (2004) introduced a proof system, which verifies whether a given CNF is unsatisfiable by encoding proof lines as OBDDs. This method was later extended to a larger family of OBDD-based proof systems. In this talk, we introduce proof systems that instead rely on SDDs, and compare them to well-known versions of OBDD-based proof systems.

In this talk, we consider the task of representing the set of all homomorphisms between two finite relational structures by tractable circuit classes from knowledge compilation. The idea is that this may allow us to greatly compress the set, while still allowing us to perform various algorithmic tasks -- such as counting and enumeration -- efficiently. This is a very general problem which can alternatively be viewed as representing the answers to a CSP or as the result of a full conjunctive query on a relational database. Because of this the problem is in general intractable, we are interested in which restrictions of the problem become tractable. In particular, we are interested in left-hand-side restrictions: for which classes of structures C, is it the case that for every A in C and every B, the set of homomorphisms from A to B has a 'small' tractable circuit. I will discuss various results related to this problem. The talk is based on joint work with Christoph Berkholz.

Abstract: We consider the following well-known story: A teacher announces to her students a test for the following week and adds that the day of the test will be “surprising”. The students use this announcement as the basis for a “logical derivation”, which leads to a contradiction. They (falsely) interpret this as saying that there cannot be a test. Nonetheless, the teacher gives a test e.g. on Wednesday, (intuitively) surprising the students. -
Its curious turns give the story a paradoxical flavor. The story runs under several alternative names, e.g. the “unexpected hanging paradox” or the “prediction paradox”. (For an informal discussion see https:// en.wikipedia.org/wiki/Unexpected_hanging_paradox.)
Discussions and analyses of the story in the philosophical and mathematical literature are abundant, spanning the period from the late 1940s until today. Apparently, none of the many explanations that have appeared has been generally accepted as conclusive and convincing.
We offer a fresh view. We give a precise formulation of “surprise relative to given knowledge”, where “surprise” is defined by a formula in propositional logic, and “knowledge” is defined as a set of axioms. We first use this to describe exactly how the argument of the students works and identify five faulty steps. Taking a more general viewpoint, we ask if one can prove anything on the basis of an initial set of axioms and the assumption that the self-referential announcement of the teacher becomes “true” (quotation marks are used on purpose). It turns out that this is not so in all but the most trivial situations where the teacher has no choice at all. The reason is that for a “rational teacher” the announcement “I will give a surprise test” does not mean more than “I can give a surprise test”. In a third part we formulate our viewpoint in system S5 of propositional modal logic. A modal formula sigma is identified that formalizes ``there will be a surprising test'',and it is shown that the students take the announcement to mean “box sigma” (“it is necessary/known that there is a surprise test”) while for a “rational teacher” they cannot conclude more than “box diamond sigma” (“it is known that it is possible that there is a surprise test”, which is much weaker).
All contradictions or "paradoxical'' issues that have been seen in the announcement vanish into thin air.
Reference: https://arxiv.org/abs/2601.19418

Abstract: A monadic decomposition of a formula over a first-order theory is an equivalent Boolean combination of atomic formulas, each containing only one variable. Monadic decomposition is a generic simplification technique that has found applications in various settings such as quantifier elimination, string solving, and constraint databases. Previous work has mostly focused on the decision problem of whether a formula admits a monadic decomposition. However, much less is known on how to actually efficiently produce a small monadic decomposition, which is required for any application.
We study this question for the quantifier-free fragment of Presburger arithmetic. Here, monadic decomposability is known to be coNP-complete, and monadic decompositions can be computed in exponential time. An exponential size lower bound was only known for monadic decompositions in DNF or CNF. In this work, we extend the exponential lower bound to general monadic decompositions. Guided by this lower bound, we present fragments that admit polynomially-sized monadic decompositions which, in many cases, can be constructed efficiently. A surprising key ingredient in our proof are small-depth circuits for arithmetic operations in Chinese remainder representation, due to Beame, Cook, Hoover (1986).

Abstract: Dependence logic is a formalism that augments the syntax of first-order logic with dependence atoms asserting that the value of a  variable is determined by the values of some other variables, i.e., dependence atoms express functional dependencies in relational databases. On finite structures, dependence logic captures NP, hence there are sentences of dependence logic  whose model-checking problem is NP-complete. In fact, it is known that there are disjunctions of three dependence atoms whose model-checking problem is NP-complete.
Motivated from considerations in database theory, we study the model-checking problem for disjunctions of two unary dependence atoms and establish a trichotomy theorem, namely, for every such formula, one of the following is true for the model-checking problem: (i) it is NL-complete; (ii) it is L-complete; (iii) it is first-order definable (hence, in AC0). Furthermore, we classify the complexity of the model-checking problem for disjunctions of two arbitrary dependence atoms, and also characterize when such a disjunction is coherent,  i.e., when it satisfies a certain  small-model property. Along the way, we identify a new class of 2CNF-formulas whose satisfiability problem is L-complete.

Abstract: Answering so-called conjunctive queries is one of the central problems in database theory and practice. In this talk, I will give an introduction into this area and show that, in some settings, its complexity can be well understood within the framework of fine-grained complexity.

Abstract: A graph is c-closed when every pair of nonadjacent vertices has at most c - 1 common neighbors. In c-Closed Vertex Deletion, the input is a graph G and an integer k and we ask whether G can be transformed into a c-closed graph by deleting at most k vertices. We study the classic and parameterized complexity of c-Closed Vertex Deletion. We obtain, for example, NP-hardness for the case that G is bipartite with bounded maximum degree. We also show upper and lower bounds on the size of problem kernels for the parameter k and introduce a new parameter, the number x of vertices in bad pairs, for which we show a problem kernel of size O(x^3 + x^2 * c)). Here, a pair of nonadjacent vertices is bad if they have at least c common neighbors. Finally, we show that c-Closed Vertex Deletion can be solved in polynomial time on unit interval graphs with depth at most c + 1 and that it is fixed-parameter tractable with respect to the neighborhood diversity of G.

Abstract: In rank aggregation problems, the task is to find a representative permutation from a collection of rankings/permutations. It plays a central role in areas such as social choice, information retrieval, and computational biology. Two fundamental aggregation tasks are the center and median problems, which minimize the maximum and the total distance to the input permutations, respectively. While these problems are well understood under Kendall’s tau and related distances, their parameterized complexity under the popular Ulam metric, an edit-distance-based metric on permutations which is closely related to longest common subsequences, has remained largely unexplored. In this work, we initiate a systematic study of the parameterized complexity and kernelization of rank aggregation under the Ulam metric. We consider both the center and median problems, as well as their generalizations to the k-center and k-median clustering settings, parameterized by the maximum distance and the total distance, respectively. In the k-center problem, the task is to decide whether there exist k center permutations such that each input permutation is within Ulam distance at most d from some center. The k-median problem analogously asks for k medians that minimize the total distance of all permutations to their respective closest median.

For these settings, we provide a comprehensive picture of the fixed-tractability landscape. Both the k-center and k-median problems are known to be NP-hard even if k = 1. Our main results include fixed-parameter tractability (FPT) algorithms when parameterized by k+d for both problems. These are accompanied by matching lower bounds for the parameterization by d alone. We further show that k-median admits a polynomial kernel when parameterized by d+k, while we rule out such a result for k-center under common complexity assumptions. The technically most interesting result is likely the FPT-algorithm for k-center, which is based on a novel local-search framework tailored to the non-local nature of Ulam moves.

Abstract: In Correlation Clustering, the input is a graph G = (V, E) together with a weight function ω : (V choose 2) → ℤ. The task is to partition the vertex set V into clusters such that the total weight of edges between clusters and missing edges inside clusters is minimized. Due to close connections between Correlation Clustering and Edge Multicut, deciding whether there exists a partition with total cost at most k is fixed-parameter tractable (FPT) with respect to k, but a polynomial kernel is presumably impossible. We study the influence of the structure of the fuzzy edge graph, that is, the graph induced by the weight-0 edges. In particular, we show that Correlation Clustering admits a polynomial kernel when parameterized by k + d, where d is the degeneracy of the fuzzy edge graph, and when parameterized by k + c, where c is the closure of the fuzzy edge graph. We complement these positive results by showing hardness for several settings where the graph induced by the edges and non-edges has very restricted structure.

Abstract: The Sandwich Problem (SP) for a graph class C is the following computational problem. The input is a pair of graphs (V,E1) and (V,E2) where E1⊆E2, and the task is to decide whether there is an edge set E where E1⊆E⊆E2 such that the graph (V,E) belongs toC. In this paper we show that many SPs correspond to the constraint satisfaction problem (CSP) of an infinite 2-edge-coloured graph H. We then notice that several known complexity results for SPs also follow from general complexity classifications of infinite-domain CSPs, suggesting a fruitful application of the theory of CSPs to complexity classifications of SPs. We strengthen this evidence by using basic tools from constraint satisfaction theory to propose new complexity results of the SP for several graph classes including line graphs of multigraphs, line graphs of bipartite multigraphs, Kk-free perfect graphs, and classes described by forbidding finitely many induced subgraphs, such as {I4,P4}-free graphs, settling an open problem of Alvarado, Dantas, and Rautenbach (2019). We also construct a graph sandwich problem which is in coNP, but neither in P nor coNP-complete (unless P = coNP).
joint work with Santiago Guzman-Pro

Abstract: Constraint satisfaction problems (CSP) are a wide class of decisions problems. They include n-colorability of graphs, Hornsat, 3-Sat, 2-Sat, reachability in undirected graphs, reachability in directed graphs and linear equations over finite fields. Some of these problems are complete for L, NL, Mod-p L, P or NP. It is known that there are no NP-intermediate CSPs, but we have no classification of the complexity classes within P. We aim to achieve such a classification by considering problems up to gadgets reductions, that is a type of log space reductions, which has an algebraic description as primitive positive construction and as minion homomorphism. In this poset of CSPs up to gadget reductions, a full list of all finite simple groups will appear.

Abstract: We investigate the possibility to separate the bisimulation-invariant fragment of P from that of NP, resp. PSPACE. We build on Otto’s Theorem stating that the bisimulation-invariant queries in P are exactly those that are definable in the polyadic mu-calculus, and use a known construction from model checking in order to reduce definability in the polyadic mu-calculus to definability in the ordinary modal mu-calculus within the class of so-called power graphs, giving rise to a notion of relative regularity. We give examples of certain bisimulation-invariant queries in NP, resp. PSPACE, and characterise their membership in P in terms of relative non-regularity of particular families of tree languages. A proof of non-regularity for all members of one such family would separate the corresponding class from P, but the combinatorial complexity involved in it is high. On the plus side, the step into the bisimulation-invariant world alleviates the order-problem that other approaches in descriptive complexity suffer from when studying the relationship between P and classes above.
This is joint work with Martin Lange (University of Kassel)