ABSTRACT. Skolem functions play a central role in the study of first order logic, both from a theoretical and practical point of view. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. The question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc. In the restricted setting of quantified Boolean formulas with a \forall^* \exists^* quantifier prefix, the problem of synthesizing Boolean Skolem functions has been studied in depth, with various recent works focusing on both theoretical and practical aspects of the problem. However, the literature is sparse in corresponding existing results for the general case of first-order logic.

In this paper, we launch an investigation into the computability aspects of Skolem functions and their automated synthesis in the full generality of first order logic. Our first main result is a negative result showing that even under very mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. Our second main result is positive; we provide a precise characterization of first-order theories that permit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations of Skolem functions. We show that several first-order theories used in applications satisfy our characterization conditions, and hence admit effective synthesis of computable Skolem interpretations. We also show that some important first-order theories fail our characterization conditions, and therefore must remain outside the ambit of automated synthesis of computable Skolem function interpretations. Finally, we present some results on when Skolem functions can be synthesized as terms in the underlying logic.

ABSTRACT. Given a set P of n points that are moving in the plane, we consider the problem of computing a spanning tree for these moving points that does not change its combinatorial structure during the point movement. The objective is to minimize the bottleneck weight of the spanning tree (i.e., the largest Euclidean length of all edges) during the whole movement. The problem was solved in O(n^2) time previously [Akitaya, Biniaz, Bose, De Carufel, Maheshwari, Silveira, and Smid, WADS 2021]. In this paper, we present a new algorithm of O(n^{4/3} log^3 n) time.

ABSTRACT. We consider a weighted counting problem on matchings, denoted~$\probmatch(\calG)$, on an arbitrary fixed graph family~$\mathcal{G}$. The input consists of a graph~$G\in \mathcal{G}$ and of rational probabilities of existence on every edge of~$G$, assuming independence. The output is the probability of obtaining a \emph{matching} of~$G$ in the resulting distribution, i.e., a set of edges that are pairwise disjoint. It is known that, if~$\mathcal{G}$ has bounded \emph{treewidth}, then~$\probmatch(\calG)$ can be solved in polynomial time. In this paper we show that, under some assumptions, bounded treewidth in fact \emph{characterizes} the tractable graph families for this problem. More precisely, we show intractability for all graph families $\calG$ satisfying the following \emph{treewidth-constructibility} requirement: given an integer~$k$ in unary, we can construct in polynomial time a graph $G \in \calG$ with treewidth at least~$k$. Our hardness result is then the following: for \emph{any} treewidth-constructible graph family~$\calG$, the problem $\probmatch(\calG)$ is intractable. This generalizes known hardness results for weighted matching counting under some restrictions that do not bound treewidth, e.g., being planar, 3-regular, or bipartite; it also answers a question left open in~\cite{amarilli2016tractable}. We also obtain a similar lower bound for the weighted counting of edge covers.

ABSTRACT. We prove that the proof system OBDD(and, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of Atserias and Muller [FOCS 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with a multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n + 1 participants was proved by Göös et. el. [STOC 2020] to establish the hardness of automatability result for Cutting Planes.

ABSTRACT. We study fundamental reachability problems for pseudo-orbits of linear dynamical systems. Pseudo-orbits can be viewed as a model of computation with limited precision and pseudo-reachability can be thought of as a robust version of classical reachability. Using an approach based on o-minimality of (the structure of) real numbers with exponentiation, we prove decidability of the discrete-time pseudo-reachability problem with arbitrary semialgebraic targets for diagonalisable linear dynamical systems. We also show that our method can be used to reduce the continuous-time pseudo-reachability problem to the (classical) time-bounded reachability problem, which is known to be conditionally decidable.

ABSTRACT. We study deterministic and randomized streaming algorithms for word problems of finitely generated groups. For finitely generated linear groups, metabelian groups and free solvable groups we show the existence of randomized streaming algorithms with logarithmic space complexity for their word problems. We also show that the class of finitely generated groups with a logspace randomized streaming algorithm for the word problem is closed under several group theoretical constructions: finite extensions, direct products, free products and wreath products by free abelian groups. We contrast these results with several lower bound. An example of a finitely presented group, where the word problem has only a linear space randomized streaming algorithm, is Thompson's group F.

ABSTRACT. CSP and SI are among the most well-studied computational problems in Computer Science. While neither problem is thought to be in PTIME, much work is done on PTIME approximations to both problems. Two such historically important approximations are the k-consistency algorithm for CSP and the k-Weisfeiler-Leman algorithm for SI, both of which are based on propagating local partial solutions. The limitations of these algorithms are well-known – k-consistency can solve precisely those CSPs of bounded width and k-Weisfeiler-Leman can only distinguish structures which differ on properties definable in C^k. In this paper, we introduce a novel sheaf-theoretic approach to CSP and SI and their approximations. We show that both problems can be viewed as deciding the existence of global sections of presheaves, H_k(A,B) and I_k(A,B) and that the success of the k-consistency and k-Weisfeiler-Leman algorithms correspond to the existence of certain efficiently computable subpresheaves of these. Furthermore, building on work of Abramsky and others in quantum foundations, we show how to use Čech cohomology in H_k(A,B) and I_k(A,B) to detect obstructions to the existence of the desired global sections and derive new efficient cohomological algorithms extending k consistency and k-Weisfeiler-Leman. We show that cohomological k-consistency can solve systems of equations over all finite rings and that cohomological Weisfeiler-Leman can distinguish positive and negative instances of the Cai-Fürer-Immerman property over several important classes of structures.

ABSTRACT. Constraint satisfaction problems (CSP) encompass an enormous variety of computational problems. In particular, all partition functions from statistical physics, such as spin systems, are special cases of counting CSP (#CSP). We prove a complete complexity classification for every counting problem in #CSP with nonnegative valued constraint functions that is valid when every variable occurs a bounded number of times in all constraints. We show that, depending on the set of constraint functions F, every problem in the complexity class #CSP(F) defined by F is either polynomial time computable for all instances without the bounded occurrence restriction, or is #P-hard even when restricted to bounded degree input instances. The constant bound in the degree depends on F. The dichotomy criterion on F is decidable. As a second contribution, we prove a slightly modified but more streamlined decision procedure for tractability. This enables us to fully classify a family of directed weighted graph homomorphism problems. This family contains both P-time tractable problems and #P-hard problems. To our best knowledge, this is the first family of such problems explicitly classified that are not acyclic, thereby the Lov\'asz-goodness criterion of Dyer-Goldberg-Paterson cannot be applied.

ABSTRACT. The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXPTIME. While in theory iterating this approach yields complete problems for k-NEXPTIME for all $k>0$, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds.

The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higher-order Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k,d), $k\ge 0$, $d\ge 1$ in which variables are interpreted as Boolean functions of order at most $k$ and there are $d$ alternations between functions of order exactly $k$. We show that the unbounded HOSAT problem is $\tower$-complete, and that HOSAT(k,d) is complete for the weak k-EXPTIME hierarchy with $d$ alternations for fixed $k,d \geq 1$. We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic.

ABSTRACT. The minimum number of clauses in a~CNF representation of the parity function $x_1 \oplus x_2 \oplus \dotsb \oplus x_n$ is $2^{n-1}$. One can obtain a~more compact CNF encoding by~using non-deterministic variables (also known as~guess or~auxiliary variables). In~this paper, we prove the following lower bounds, that almost match known upper bounds, on~the number~$m$ of~clauses and the maximum width~$k$ of clauses: 1)~if there are at~most $s$~auxiliary variables, then $m \ge \Omega\left(2^{n/(s+1)}/n\right)$ and $k \ge n/(s+1)$; 2)~the minimum number of clauses is at~least~$3n$. We~derive the first two bounds from the Satisfiability Coding Lemma due to~Paturi, Pudl{\'{a}}k, and Zane.

ABSTRACT. Hybrid logic is a widely-studied extension of basic modal logic, which corresponds to the bounded fragment of first-order logic. We study it from two novel perspectives: (1) We apply the recently introduced paradigm of comonadic semantics, which provides a new set of tools drawing on ideas from categorical semantics which can be applied to finite model theory, descriptive complexity and combinatorics. (2) We give a novel semantic characterization of hybrid logic in terms of invariance under disjoint extensions, a minimal form of locality. A notable feature of this result is that we give a uniform proof, valid for both the finite and infinite cases.

ABSTRACT. The Caus[-] construction takes a compact closed category of basic processes and yields a *-autonomous category of higher-order processes obeying certain signalling/causality constraints, as dictated by the type system in the resulting category. This paper looks at instances where the base category C satisfies additional properties yielding an affine-linear structure on Caus[C] and a substantially richer internal logic. While the original construction only gave multiplicative linear logic, here we additionally obtain additives and a non-commutative, self-dual sequential product yielding a model of Guglielmi's BV logic. Furthermore, we obtain a natural interpretation for the sequential product as "A can signal to B, but not vice-versa", which sits as expected between the non-signalling tensor and the fully-signalling (i.e. unconstrained) par. Fixing matrices of positive numbers for C recovers the BV category structure of probabilistic coherence spaces identified by Blute, Panangaden, and Slavnov, restricted to normalised maps. On the other hand, fixing the category of completely positive maps gives an entirely new model of BV consisting of higher order quantum channels, encompassing recent work in the study of quantum and indefinite causal structures.

ABSTRACT. We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it.

We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO à la van Benthem.

Afterwards, we study the Craig Interpolation Property (CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the ``forwardness'' of our logics.

ABSTRACT. When we bundle quantifiers and modalities together (as in $\exists x \Box$, $\Diamond \forall x$ etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting \textit{bundled} fragments of FOML. It is well-known that finding decidable fragments of \FOML is hard, but existing work shows that certain bundled fragments are decidable [Padmanabha et al 2018], without any restriction on the arity of predicates, the number of variables, or the modal scope. In this paper, we explore generalized bundles such as $\forall x\forall y \Box, \forall x\exists y \Diamond$ etc., and map the terrain with regard to decidability, presenting both decidability and undecidability results. In particular, we propose the loosely bundled fragment which is decidable over increasing domains and encompasses all known decidable bundled fragments.