MFCS 2025: 50TH INTERNATIONAL SYMPOSIUM ON MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE
PROGRAM FOR TUESDAY, AUGUST 26TH
Days:
previous day
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 5
Location: 316 (Main room)
09:00
On Graph Queries and Modal Constraints

ABSTRACT. Some fundamental problems in database theory and knowledge representation can be viewed as instances of the query entailment problem. While query evaluation asks whether a given query holds in a specific structure, query entailment consists in determining whether the query holds in every model of a given theory that extends that structure. The input structure represents the raw data stored in a database; the theory captures contextual information such as a set of database constraints or an ontology; and the query is used to extract specific information of interest. The recent proliferation of graph databases has brought the database and knowledge representa- tion communities closer together, as many key problems in both fields involve the same structures – labelled graphs – and similar combinations of formalisms for theories and queries. A notable example is the combination of description logics and conjunctive regular path queries. Description logics are a family of formalisms based on fragments of first order logic, akin to modal logics. They are among the most prominent ontology languages and they are capable of expressing most kinds of constraints relevant in graph databases. Conjunctive regular path queries extend conjunctive queries (primitive positive first-order formulas) by allowing regular expressions over binary predicates to be used as atoms. They form the core of practical query languages employed in graph database systems and the Semantic Web. What distinguishes the two fields is the approach to infinity: knowledge representation embraces infinite models, whereas database theory focuses on finite models. Although many cases of the entailment problem have long been solved over unrestricted (finite or infinite) models, their finite- model counterparts have only recently seen progress, and many questions remain open.

10:00-10:30Coffee Break
10:30-11:45 Session 6A
Location: 316 (Main room)
10:30
An EPTAS for minimizing the total weighted completion time of jobs with release dates on uniformly related machines

ABSTRACT. Scheduling of independent jobs with release dates so as to minimize the total weighted completion time is a well-known scheduling problem. Here, we study it for the classic machine environment of uniformly related machines. An efficient polynomial time approximation scheme (an EPTAS) is a family of (1+epsilon)-approximation algorithms where the running time is bounded by a polynomial in the input size times a function of epsilon>0. For problems that are NP-hard in the strong sense, as it is the case for the problem studied here, an EPTAS is the best possible approximation scheme. We design an EPTAS for the problem by employing known techniques and introducing a large collection of new methods.

10:55
Counting Locally Optimal Tours in the TSP

ABSTRACT. We show that the problem of counting 2-optimal tours in instances of the Travelling Salesperson Problem (TSP) on complete graphs is #P-complete. In addition, we show that the expected number of 2-optimal tours in random instances of the TSP on complete graphs is $O(1.2098^n \sqrt{n!})$. Based on numerical experiments, we conjecture that the true bound is at most $O(\sqrt{n!})$, which is approximately the square root of the total number of tours.

11:20
Approximating Prize-Collecting Variants of TSP

ABSTRACT. We present an approximation algorithm for the Prize-collecting Ordered Traveling Salesman Problem (PCOTSP), which simultaneously generalizes the Prize-collecting TSP and the Ordered TSP. The Prize-collecting TSP is well-studied and has a long history, with the current best approximation factor slightly below 1.6, shown by Blauth, Klein and Nägele [IPCO 2024]. The best approximation ratio for Ordered TSP is 3/2+1/e , presented by Böhm, Friggstad, Mömke, Spoerhase [SODA 2025] and Armbruster, Mnich, Nägele [Approx 2024]. The former also present a factor 2.2131 approximation algorithm for Multi-Path-TSP. We present a 2.097-approximation algorithm for PCOTSP, which is, to the best of our knowledge, the first result for this problem. Key ideas in our approach are to sample a set of trees and then to probabilistically pick up some vertices, and to use the pruning ideas of Blauth, Klein, Nägele [IPCO 2024] on the sampled vertices. While the sampling probability of vertices for our problem is lower than for PCTSP, intuitively leaving less spare penalty to spend, we leverage the cycle structure induced by the sampled trees together with a simple combinatorial algorithm to bring the approximation factor below 2.1. Our techniques extend to Prize-collecting Multi-Path TSP, building on results from Böhm, Friggstad, Mömke, Spoerhase [SODA 2025], leading to a 2.41-approximation.

10:30-11:45 Session 6B
10:30
Resolving Nondeterminism with Randomness

ABSTRACT. We define and study classes of $\omega$-regular automata for which the nondeterminism can be resolved by a policy that uses a combination of memory and randomness on any input word, based solely on the prefix read so far. We examine two settings for providing the input word to an automaton. In the first setting, called \emph{adversarial resolvability}, the input word is constructed letter-by-letter by an adversary, dependent on the resolver’s previous decisions. In the second setting, called \emph{stochastic resolvability}, the adversary pre-commits to an infinite word and reveals it letter-by-letter. In each setting, we require the existence of an almost-sure resolver, i.e., a policy that ensures that as long as the adversary provides a word in the language of the underlying nondeterministic automaton, the run constructed by the policy is accepting with probability~1.

The class of automata that are adversarially resolvable is the well-studied class of history-deterministic automata. The case of stochastically resolvable automata, on the other hand, defines a novel class. Restricting the class of resolvers in both settings to stochastic policies without memory introduces two additional new classes of automata.

10:55
Relative randomness and continuous translation functions

ABSTRACT. Solovay reducibility, a central object of study in algorithmic randomness, is defined via translation functions that map approximations of a real to approximations of another real. In what follows, we examine different notions of translation functions and corresponding variants of Solovay reducibility.

The main result of this article, Theorem 19, is a generalization of the Barmpalias--Lewis-Pye Limit Theorem [DOI:10.1016/j.jcss.2017.06.002] to the reducibility cl-open firstly appeared in the work of Kumabe, Miyabe, and Suzuki [DOI:10.3233/COM-230486] in 2024. Furthermore, we deduce from the main result an equivalent characteristic of Martin-Löf randomness on the set of left-c.e. reals in terms of cl-open-reducibility of a real to itself.

11:20
Random Permutations in Computational Complexity

ABSTRACT. Classical results of Bennett and Gill (1981) show that with probability 1, $\P^A \neq \NP^A$ relative to a random oracle $A$, and with probability 1, $\P^\pi \neq \NP^\pi \cap \coNP^\pi$ relative to a random permutation $\pi$. Whether $\P^A = \NP^A \cap \coNP^A$ holds relative to a random oracle $A$ remains open. While the random oracle separation has been extended to specific individually random oracles--such as Martin-Löf random or resource-bounded random oracles--no analogous result is known for individually random permutations.

We introduce a new resource-bounded measure framework for analyzing individually random permutations. We define permutation martingales and permutation betting games that characterize measure-zero sets in the space of permutations, enabling formal definitions of polynomial-time random permutations, polynomial-time betting-game random permutations, and polynomial-space random permutations.

Our main result shows that $\P^\pi \neq \NP^\pi \cap \coNP^\pi$ for every polynomial-time betting-game random permutation $\pi$. This is the first separation result relative to individually random permutations, rather than an almost-everywhere separation. We also strengthen a quantum separation of Bennett, Bernstein, Brassard, and Vazirani (1997) by showing that $\NP^\pi \cap \coNP^\pi \not\subseteq \BQP^\pi$ for every polynomial-space random permutation $\pi$.

We investigate the relationship between random permutations and random oracles. We prove that random oracles are polynomial-time reducible from random permutations. The converse--whether every random permutation is reducible from a random oracle--remains open. We show that if $\NP \cap \coNP$ is not a measurable subset of $\EXP$, then $\P^A \neq \NP^A \cap \coNP^A$ holds with probability 1 relative to a random oracle $A$. Conversely, establishing this random oracle separation with time-bounded measure would imply $\BPP$ is a measure 0 subset of $\EXP$.

Our framework builds a foundation for studying permutation-based complexity using resource-bounded measure, in direct analogy to classical work on random oracles. It raises natural questions about the power and limitations of random permutations, their relationship to random oracles, and whether individual randomness can yield new class separations.

11:45-14:15Lunch Break
14:15-15:30 Session 7A
Location: 316 (Main room)
14:15
Counting Distinct Square Substrings in Sublinear Time

ABSTRACT. We show that the number of distinct squares in a packed string of length n over an alphabet of size \sigma can be computed in O(n / \log_{\sigma} n) time in the word-RAM model of computation. This paper is the first to introduce a sublinear time algorithm for the packed version of squares counting. The packed representation of a string of length n over an alphabet of size \sigma is given as a sequence of O(n / \log_{\sigma} n) machine words in the word-RAM model (a machine word consists of \omega \ge \log_2 n bits).

Previously it was known how to count distinct squares in O(n) time [Gusfield and Stoye, JCSS 2004], even for a string over an integer alphabet, see [Crochemore et al., TCS 2014; Bannai et al., CPM 2017; Charalampopoulos et al., SPIRE 2020]. We use techniques of squares extraction from runs described in [Crochemore et al., TCS 2014]. However, the packed model requires novel approaches. In particular, we need an O(n / \log_{\sigma} n) sized representation of all long-period runs (runs with periods that are \Omega(\log_{\sigma} n)) which guarantees sublinear time counting of potentially linearly-many implied squares. The long-period runs with a string period that is periodic itself (called \emph{layer runs}) are an obstacle, since their number is \Omega(n). Fortunately, the number of all other long-period runs is sublinear and we can construct their explicit representations in O(n / \log_{\sigma} n) time by adopting the insights of Amir et al. [ESA 2019], combined with sublinear time tools provided by the \pillar model of computations in case of packed strings. A sublinear time squares-counting in layer runs is achieved by exploiting combinatorial properties of types of pyramidally-shaped groups of layer runs. As a by-product, we discover several new interesting structural properties of runs.

Another difficulty is to compute, in sublinear time, locations of Lyndon roots of runs in packed strings, which is needed for grouping of runs that can generate equal squares. To overcome this difficulty, we introduce sparse-Lyndon roots which are based on the notion of string synchronizers proposed by Kempa and Kociumaka [STOC 2019].

14:40
A proof of Shur's conjecture on the growth of power-free languages over large alphabets

ABSTRACT. We settle a conjecture of Shur on an estimation of the exponential growth rates of the languages of $\left(\frac{n}{n-1}\right)$-free words and $\left(\frac{n}{n-1}\right)^+$-free words over large alphabets of size $k$ with a correction of order $O\left(\frac{1}{k^2}\right)$.

15:05
Reachability in symmetric VASS

ABSTRACT. We investigate the reachability problem in symmetric vector addition systems with states (VASS), where transitions are invariant under a group of permutations of coordinates. One extremal case, the trivial groups, yields general VASS. In another extremal case, the symmetric groups, we show that the reachability problem can be solved in PSPACE, regardless of the dimension of input VASS (to be contrasted with Ackermannian complexity in general VASS). We also consider other groups, in particular alternating and cyclic ones. Furthermore, motivated by open status of the reachability problem in data VASS, we estimate the gain in complexity when the group arises as a combination of trivial and symmetric group.

14:15-15:30 Session 7B
14:15
Polynomial-time Tractable Problems over the p-adic Numbers

ABSTRACT. We study the computational complexity of fundamental problems over the p-adic numbers Q_p and the p-adic integers Z_p. Guépin, Haase, and Worrell proved that checking satisfiability of systems of linear equations combined with valuation constraints of the form v_p(x) = c for p \geq 5 is NP-complete (both over Z_p and over Q_p), and left the cases p=2 and p=3 open. We solve their problem by showing that the problem is NP-complete for Z_3 and for Q_3, but that it is in P for Z_2 and for Q_2. We also present different polynomial-time algorithms for solvability of systems of linear equations in Q_p with either constraints of the form v_p(x) \leq c or of the form v_p(x)\geq c for c in Z. Finally, we show how our algorithms can be used to decide in polynomial time the satisfiability of systems of (strict and non-strict) linear inequalities over Q together with valuation constraints v_p(x) \geq c for several different prime numbers p simultaneously.

14:40
Deciding Robust Instances of an Escape Problem for Dynamical Systems in Euclidean Space

ABSTRACT. We study the problem of deciding whether a point escapes a closed subset of $\R^d$ under the iteration of a continuous map $f \colon \R^d \to \R^d$ in the bit-model of real computation. We give a sound partial decision method for this problem which is complete in the sense that its halting set contains the halting set of all sound partial decision methods for the problem. Equivalently, our decision method terminates on all problem instances whose answer is robust under all sufficiently small perturbations of the function. We further show that the halting set of our algorithm is dense in the set of all problem instances. While our algorithm applies to general continuous functions, we demonstrate that it also yields complete decision methods for much more rigid function families: affine linear systems and quadratic complex polynomials. In the latter case, completeness is subject to the density of hyperbolicity conjecture in complex dynamics. This in particular yields an alternative proof of Hertling's (2004) conditional answer to a question raised by Penrose (1989) regarding the computability of the Mandelbrot set.

15:05
One-Parametric Presburger Arithmetic has Quantifier Elimination

ABSTRACT. We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function (x -> t*x), where t is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al., Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions (x -> floor(x/f(t))), one for each integer polynomial f.

Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring Z[t] of univariate polynomials. The second is reminiscent of the so-called "base t division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size.

15:30-16:00Coffee Break
16:00-17:15 Session 8A
Location: 316 (Main room)
16:00
Linear Time Subsequence and Supersequence Regex Matching

ABSTRACT. It is well-known that checking whether a given string $w$ matches a given regular expression $r$ can be done in quadratic time $O(|w|\cdot |r|)$ and that this cannot be improved to a truly subquadratic running time of $O((|w|\cdot |r|)^{1-\epsilon})$ assuming the strong exponential time hypothesis (SETH).

We study a different matching paradigm where we ask instead whether $w$ has a subsequence that matches $r$, and show that regex matching in this sense can be solved in linear time $O(|w| + |r|)$. Further, the same holds if we ask for a supersequence. We show that the quantitative variants where we want to compute a longest or shortest subsequence or supersequence of $w$ that matches $r$ can be solved in $O(|w|\cdot |r|)$, i.\,e., asymptotically no worse than classical regex matching; and we show that $O(|w| + |r|)$ is conditionally not possible for these problems. We also investigate these questions with respect to other natural string relations like the infix, prefix, left-extension or extension relation instead of the subsequence and supersequence relation. We further study the complexity of the universal problem where we ask if all subsequences (or supersequences, infixes, prefixes, left-extensions or extensions) of an input string satisfy a given regular expression.

16:25
Efficient Matching of Some Fundamental Regular Expressions with Backreferences

ABSTRACT. Regular expression matching is of practical importance due to its widespread use in real-world applications. In practical use, regular expressions are often used with real-world extensions. Accordingly, the matching problem of regular expressions with real-world extensions has been actively studied in recent years, yielding steady progress. However, backreference, a popular extension supported by most modern programming languages such as Java, Python, JavaScript and others in their standard libraries for string processing, is an exception to this positive trend. In fact, it is known that the matching problem of regular expressions with backreferences (rewbs) is theoretically hard and the existence of an asymptotically fast matching algorithm for arbitrary rewbs seems unlikely. Even among currently known partial solutions, the balance between efficiency and generality remains unsatisfactory. To bridge this gap, we present an efficient matching algorithm for rewbs of the form $e_0 (e)_1 e_1 \backslash 1 e_2$ where $e_0, e, e_1, e_2$ are pure regular expressions, which are fundamental and frequently used in practical applications. It runs in quadratic time with respect to the input string length, substantially improving the best-known cubic time complexity for these rewbs. Our algorithm combines ideas from both stringology and automata theory in a novel way. We leverage two techniques from automata theory, injection and summarization, to simultaneously examine matches whose backreferenced substrings are either a fixed right-maximal repeat or its extendable prefixes, which are concepts from stringology. By further utilizing a subtle property of extendable prefixes, our algorithm correctly decides the matching problem while achieving the quadratic-time complexity.

16:50
Negated String Containment is Decidable

ABSTRACT. We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly, we show that the predicate not-contains(x1 ... xn, y1 ... ym), where x1 ... xn and y1 ... ym are sequences of string variables constrained by regular languages, is decidable. Decidability of a not-contains predicate combined with chain-free word equations and regular membership constraints follows.

16:00-17:15 Session 8B
16:00
Model-theoretic Forcing in Transition Algebra

ABSTRACT. We study Löwenheim-Skolem and Omitting Types theorems in Transition Algebra, a logical system obtained by enhancing many sorted first-order logic with features from dynamic logic. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to actions in dynamic logics to define necessity and possibility operators. We show that Upward Löwenheim-Skolem theorem, any form of compactness, and joint Robinson consistency property fail due to the expressivity of transitive closures of transitions. In this non-compact many-sorted logical system, we develop a forcing technique method by generalizing the classical method of forcing used by Keisler to prove Omitting Types theorem. Instead of working within a single signature, we work with a directed diagram of signatures, which allows us to establish Downward Löwenheim-Skolem and Omitting Types theorems despite the fact that models interpret sorts as sets, possibly empty. Building on a complete system of proof rules for Transition Algebra, we extend it with additional proof rules to reason about constructor-based and/or finite transition algebras. We then establish the completeness of this extended system for a fragment of Transition Algebra obtained by restricting models to constructor-based and/or finite transition algebras.

16:25
Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification

ABSTRACT. The notion of homomorphism indistinguishability offers a combinatorial framework for characterizing equivalences in counting logics within finite model theory. That is, for certain graph classes, two structures agree on all homomorphism counts from the class if and only if they satisfy the same sentences in a corresponding logic.This perspective often reveals connections between the combinatorial properties of graph classes and the syntactic structure of logical fragments. In this work, we extend this perspective to logics with restricted requantification, refining the stratification of logical resources in finite-variable counting logics. Specifically, we generalize Lovász-type theorems for these logics with either restricted conjunction or bounded quantifier-rank and present new combinatorial proofs of existing results. To this end, we introduce novel path and tree decompositions that incorporate the concept of reusability and develop characterizations based on pursuit-evasion games. Leveraging this framework, we establish that classes of bounded pathwidth and treewidth with reusability constraints are homomorphism distinguishing closed. Finally, we develop a comonadic perspective on requantification by constructing new comonads that encapsulate restricted-reusability pebble games. We show a tight correspondence between their coalgebras and path/tree decompositions, yielding categorical characterizations of reusability in graph decompositions. This unifies logical, combinatorial, and categorical perspectives on the notion of reusability.

16:50
Symmetric Proofs in the Ideal Proof System

ABSTRACT. We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.