Abstracts for pre-conference workshop
The Complexity of Enumerating Satisfying Assignments
We study the algorithmic problem to enumerate all satisfying assignments of a given propositional formula. Well known is that for formula classes with a polynomial-time decision problem, this can be done within the class DelayP, introduced by Johnson, Papadimitriou and Yannakakis in 1988 and regarded since then as a reasonable notion of “efficient” enumeration.
We will present two results:
- We generalize the class DelayP to a hierarchy analogous to the polynomial-time hierarchy of decision problems and show that Enum-SAT is complete in the Sigma_1 level of this hierarchy under some form of enumeration Turing reductions.
- We define a hierarchy of very efficiently enumerable problems within DelayP, based on the Boolean circuit class AC_0, and place the enumeration problems for monotone, IHS, Krom, and affine formulas in lower levels of this hierarchy.
Open remains an exact classification of the problem Enum-Horn-SAT.
Reducing Stochastic Games to Semidefinite Programming
We present a polynomial-time reduction from max-average constraints to the feasibility problem for semidefinite programs. This shows that Condon's simple stochastic games, stochastic mean payoff games, and in particular mean payoff games and parity games can all be reduced to semidefinite programming.
Graph Neural Networks and Arithmetic Circuits
We characterize the computational power of neural networks that follow the graph neural network (GNN) architecture, not restricted to aggregate-combine GNNs or other particular types. We establish an exact correspondence between the expressivity of GNNs using diverse activation functions and arithmetic circuits over real numbers. In our results the activation function of the network becomes a gate type in the circuit. Our result holds for families of constant depth circuits and networks, both uniformly and non-uniformly, for all common activation functions.
The complexity of computing the period and the exponent of a digraph
The period of a strongly connected digraph is the greatest common divisor of the lengths of all its cycles. The period of a digraph is the least common multiple of the periods of its strongly connected components that contain at least one cycle. These notions play an important role in the theory of Markov chains and the analysis of powers of nonnegative matrices. While the time complexity of computing the period is well-understood, little is known about its space complexity. We show that the problem of computing the period of a digraph is NL-complete, even if all its cycles are contained in the same strongly connected component. However, if the digraph is strongly connected, we show that this problem becomes L-complete. For primitive digraphs (that is, strongly connected digraphs of period one), there always exists a number m such that there is a path of length exactly m between every two vertices. We show that computing the smallest such m, called the exponent of a digraph, is NL-complete. The exponent of a primitive digraph is a particular case of the index of convergence of a nonnegative matrix, which we also show to be computable in NL, and thus NL-complete.
This is a joint work with Stefan Kiefer. Arxiv pre-print: 2408.05762
Optimal Proof Systems for Complex Sets are Hard to Find
The study of proof systems was initially motivated by the NP versus coNP question. Cook and Reckhow [CR79] define a proof system for a set L as a polynomial-time computable function f whose range is L. They show that NP = coNP if and only if there exists a proof system with polynomial-size proofs for the set of propositional tautologies (TAUT). Hence, in order to show NP≠coNP, it suffices to rule out polynomial-size proofs for increasingly powerful proof systems for TAUT. This approach to the NP versus coNP question is known as the Cook-Reckhow program. Krajíček and Pudlák [KP89] capture the idea of a most powerful proof system with their notions of optimal and p-optimal proof systems. A proof system is optimal for a set L if its proofs are at most polynomially longer than proofs in any other proof system for L.
The following is a longstanding open question which was raised by Krajíček and Pudlák [KP89], Sadowski [Sad97], Köbler and Messner [KM98] and Messner [Mes00]:
Are there (arbitrarily complex) sets outside NP with optimal proof systems?
Over the past decades, this question has been investigated across multiple contexts. The first part of this talk will be an overview of the motivation for the study of optimal proof systems and review known results on necessary and sufficient conditions for their existence. The second part will present new oracle results proving the difficulty of this question.
Dynamics of Schelling Games
The emergence of homogeneous neighborhoods in cities is the outcome of the complex interaction of selfish agents. This setting can be modeled as a strategic game and methods from Algorithmic Game Theory can be employed to rigorously analyze it.
In this talk I will present case studies for game-theoretic models of residential segregation. In particular, I will focus on the study of game dynamics via potential function analysis. With the use of this concept, I will present insights into when and why residential patterns in cities stabilize over time.
Hereditary First-Order Logic and Extensional ESO
We consider two families of computational problems. The first ones are de- scribed by a fixed first-order sentence ϕ, and given an input structure A the task is to decide A satisfies ϕ hereditarily, i.e., if every (non-empty) substructure of A satisfies ϕ. These family of problems is described by hereditary first-order logic (HerFO). The second class consists of problems described by a fixed existential second order (ESO) sentence Ψ, and given an input structure A, the task if to decide if there is an extension B of A that satisfies the first-order part of Ψ, i.e., a structure B such that RA ⊆ RB for every existentially quantified predicate R of Ψ, and RA = RB for every non-quantified predicate R of Ψ. Extensional ESO is a fragment of ESO that captures these problems. In particular it describes all conservative (pre-coloured) finite-domain CSPs.
In this talk we see that extensional ESO and HerFO have the same computational power: the complement of every problem in HerFO is polynomial-time equivalent to a problem in extensional ESO, and vice versa. We also show that extensional ESO describes all CSPs of finitely bounded structures, suggesting no P vs. NP-hard dichotomy for this logic, or for HerFO. However, we also observe that extensional ESO does not have the full computational power of NP: there are problems in NP that are not polynomial-time equivalent to a problem in extensional ESO (unless E=NE) — complementarily, HerFO does not have the full computational power of coNP. If time permits, we will conclude with a description of the quantifier-prefixes for ϕ such that hereditarily checking ϕ is in P; we show that for every other quantifier-prefix there exists a formula ϕ with this prefix such that hereditarily checking ϕ is coNP-complete.
This is based on joint work with Manuel Bodirsky.
Quicksort, Timsort, Powersort - Algorithmic ideas, engineering tricks, and trivia behind CPython’s new sorting algorithm
In 2002, Tim Peters invented Timsort, a clever Mergesort variant, for the CPython reference implementation of the Python programming language. Timsort is both effective in Python and a popular export product: it is used in many languages and frameworks, notably OpenJDK, the Android runtime, and the V8 JavaScript engine. Despite its widespread use, algorithms researchers eventually discovered two flaws in Timsort's underlying algorithm: The first could lead to a stack overflow in CPython and Java; although meanwhile fixed, it exposed conceptual intricacies of the algorithm. The second flaw concerns its performance: the order in which detected sorted segments, the “runs” of the input, are merged, can be 50% more costly than necessary.
Based on ideas from optimal alphabetic trees, our Powersort merge policy finds nearly optimal merging orders with negligible overhead and using a much more transparent rule. Since Python 3.11, it is part of the CPython reference implementation. The talk will describe the involved algorithms assuming no prior familiarity.
On the Tightness of the Standard Lower Bound in the Two-Machine Routing Open Shop
In classical machine scheduling, machines typically are allowed to begin processing a new job immediately after completing the previous one. However, such schedules may be impractical in real-world applications due to necessary delays between operations. One approach to model such delays is routing shop scheduling, where jobs are located at nodes of a transportation network, and mobile machines must travel between them to perform processing. All machines start at a common depot and must return there after completing all jobs. This problem integrates shop scheduling with the well-known traveling salesman problem (TSP), significantly increasing complexity. We consider the two-machine routing open shop problem, which is NP-hard even in the simplest case with only two nodes. For a general transportation network, two best-known approximation algorithms in terms of the standard lower bound are known. The first is polynomial and has a worst-case performance guarantee of 13/8. The second achieves a 4/3-approximation, although its running time includes solving the optimal TSP. While the second algorithm is not necessarily polynomial, its properties provide important insight into the tightness of the standard lower bound: for any instance of the two-machine routing open shop problem, the optimal solution does not exceed 4/3 of the standard lower bound. In this talk, we will discuss potential approaches to narrowing this gap between the standard lower bound and the optimum in the worst case.
Categorizing Ensembles of Real-Valued Functions
The calculus of influence (B./Lange/Möller, Cade'23) facilitates formal reasoning on the behavior continuous functions in the context of classroom natural sciences experiments. It provides inference rules for simple statements on the behavior of ensembles of real-valued, continuous functions that describe the behavior of a natural sciences experiment. Typical statements express whether a function has a certain range on a given domain, and/or whether it is monotonic, antitonic, constant, or (potentially) neither of those on said domain. The purpose of the calculus is to automatically decide whether a student's hypothesis in a natural sciences experiment is valid, i.e., follows logically from known facts.
The calculus of influence is complete (relative to logical entailment for sets of such statements) for a restricted class of function ensembles, but expanding completeness to a more general setting would require the introduction of rather complicated reasoning patterns incompatible with the intended classroom use.
In this talk, we establish a new approach to decide logical entailment. Instead of refining the calculus, we refine potential statements on the behavior of function ensembles. This yields an equivalence relation of sufficient detail, but of finite index, such that logical entailment of sets of statements can be decided by an exhaustive search of the corresponding equivalence classes. The main difficulty is to accurately capture the interplay between several interacting real-valued functions to a sufficient degree, but to maintain finite index of the equivalence relation.
This is joint work with Martin Lange and Sören Möller (both University of Kassel).