We investigate the expressive power of generalized quantifiers closed under partial polymorphism conditions motivated by the study of constraint satisfaction problems. We answer a number of questions arising from the work of Dawar and Hella (CSL 2024) where such quantifiers were introduced. For quantifiers closed under partial near-unanimity polymorphisms, we establish hierarchy results clarifying the interplay between the arity of the polymorphisms and of the quantifiers: The expressive power of $(\ell+1)$-ary quantifiers closed under $\ell$-ary partial near-unanimity polymorphisms is strictly between the class of all quantifiers of arity $\ell-1$ and $\ell$. We also establish an infinite hierarchy based on the arity of quantifiers with a fixed arity of partial near-unanimity polymorphisms. Finally, we prove inexpressiveness results for quantifiers with a partial Maltsev polymorphism. The separation results are proved using novel algebraic constructions in the style of Cai-Fürer-Immerman and the quantifier pebble games of Dawar and Hella (2024).

We study the status of classical model-theoretic preservation theorems such as the Łoś-Tarski theorem and the homomorphism preservation theorem in the context of semiring semantics. Semiring semantics has its origins in the provenance analysis of database queries but has been extended to a systematic way of evaluating logical statements to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. The systematic development of semiring semantics for first-order logic and other logical systems raises the question to what extent classical model-theoretic results can be generalised to this setting and how such results depend on the underlying semiring. The definitions of semantic properties such as preservation under extensions, substructures, or homomorphisms naturally generalise to the setting of semiring semantics. However, the status of the corresponding preservation theorem strongly depends on the algebraic properties of the particular semirings. We prove that these preservation theorems do indeed hold for all lattice semirings (a quite large class, encompassing practically relevant semirings and in particular all min-max semirings). The proofs combine adaptations of the classical compactness and amalgamation methods with specific reduction methods for logical entailment that have been developed in semiring semantics. On the other side, variants of the existential preservation theorem fail for many other semirings, including the tropical semiring, the Viterbi semiring, the Łukasiewicz semiring, and the natural semirings ℕ and ℕ^∞. Surprisingly, the existential preservation theorem does hold for finite interpretations in a number of semirings, including the three-element min-max semiring, which extends the Boolean by just a single additional truth value. Thus, the situation for these semirings is in sharp contrast to the Boolean case, where the Łoś-Tarski theorem holds in general, but not in the finite.

A notorious open question in circuit complexity is whether Boolean operations of arbitrary arity can efficiently be expressed using modular counting gates only. Håstad’s celebrated switching lemma yields exponential lower bounds for the dual problem - realising modular arithmetic with Boolean gates - but, a similar lower bound for modular circuits computing the Boolean AND function has remained elusive for almost 30 years. We solve this problem for the restricted model of symmetric circuits: We consider MOD_m-circuits of arbitrary depth, and for an arbitrary modulus m ∈ ℕ, and obtain subexponential lower bounds for computing the n-ary Boolean AND function, under the assumption that the circuits are syntactically symmetric under all permutations of their n input gates. This lower bound is matched precisely by a construction due to (Idziak, Kawałek, Krzaczkowski, LICS'22), leading to the surprising conclusion that the optimal symmetric circuit size is already achieved with depth 2. Motivated by another construction from (LICS'22), which achieves smaller size at the cost of greater depth, we also prove tight size lower bounds for circuits with a more liberal notion of symmetry characterised by a nested block structure on the input variables.

The central open question of algebraic complexity is whether VP ≠ VNP, which is saying that the permanent cannot be represented by families of polynomial-size algebraic circuits. For symmetric algebraic circuits, this has been confirmed by Dawar and Wilsenach (2020), who showed exponential lower bounds on the size of symmetric circuits for the permanent. In this work, we set out to develop a more general symmetric algebraic complexity theory. Our main result is that a family of symmetric polynomials admits small symmetric circuits if and only if they can be written as a linear combination of homomorphism counting polynomials of graphs of bounded treewidth. We also establish a relationship between the symmetric complexity of subgraph counting polynomials and the vertex cover number of the pattern graph. As a concrete example, we examine the symmetric complexity of immanant families (a generalisation of the determinant and permanent) and show that a known conditional dichotomy due to Curticapean (2021) holds unconditionally in the symmetric setting.

Valiant's conjecture from 1979 asserts that the circuit complexity classes VP and VNP are distinct, meaning that the permanent does not admit polynomial-size algebraic circuits. As it is the case in many branches of complexity theory, the unconditional separation of these complexity classes seems elusive. In stark contrast, the symmetric analogue of Valiant's conjecture has been proven by Dawar and Wilsenach (ICALP 2020): the permanent does not admit symmetric algebraic circuits of polynomial size, while the determinant does. Symmetric algebraic circuits are both a powerful computational model and amenable to proving unconditional lower bounds.

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.

Abramsky, Dawar, and Wang (2017) introduced the pebbling comonad for k-variable counting logic and thereby initiated a line of work that imports category theoretic machinery to finite model theory. Such game comonads have been developed for various logics, yielding characterisations of logical equivalences in terms of isomorphisms in the associated co-Kleisli category. We show a first limitation of this approach by studying linear-algebraic logic, which is strictly more expressive than first-order counting logic and whose k-variable logical equivalence relations are known as invertible-map equivalences (IM). We show that there exists no finite-rank comonad on the category of graphs whose co-Kleisli isomorphisms characterise IM-equivalence, answering a question of Ó Conghaile and Dawar (CSL 2021). We obtain this result by ruling out a characterisation of IM-equivalence in terms of homomorphism indistinguishability and employing the Lovász-type theorems for game comonads established by Dawar, Jakl, and Reggio (2021). Two graphs are homomorphism indistinguishable over a graph class if they admit the same number of homomorphisms from every graph in the class. The IM-equivalences cannot be characterised in this way, neither when counting homomorphisms in the natural numbers, nor in any finite prime field.

The search for a logic capturing PTIME is a long standing open problem in finite model theory. One of the most promising candidate logics for this is Choiceless Polynomial Time with counting (CPT). Abstractly speaking, CPT is an isomorphism-invariant computation model working with hereditarily finite sets as data structures. While it is easy to check that the evaluation of CPT-sentences is possible in polynomial time, the converse has been open for more than 20 years: Can every PTIME-decidable property of finite structures be expressed in CPT? We attempt to make progress towards a negative answer and show that Choiceless Polynomial Time cannot compute a preorder with colour classes of logarithmic size in every hypercube. The reason is that such preorders have super-polynomially many automorphic images, which makes it impossible for CPT to define them. While the computation of such a preorder is not a decision problem that would immediately separate P and CPT, it is significant for the following reason: The so-called Cai-Fürer-Immerman (CFI) problem is one of the standard "benchmarks" for logics and maybe best known for separating fixed-point logic with counting (FPC) from P. Hence, it is natural to consider this also a potential candidate for the separation of CPT and P. The strongest known positive result in this regard says that CPT is able to solve CFI if a preorder with logarithmically sized colour classes is present in the input structure. Our result implies that this approach cannot be generalised to unordered inputs. In other words, CFI on unordered hypercubes is a PTIME-problem which provably cannot be tackled with the state-of-the-art choiceless algorithmic techniques.

We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded-width resolution, and the monomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded-width resolution captures existential least fixed-point logic, and that the polynomial calculus with bounded degree over the rationals solves precisely the problems definable in fixed-point logic with counting. We also study the bounded-degree polynomial calculus. Over the rationals, it captures fixed-point logic with counting if we restrict the bit-complexity of the coefficients. For unrestricted coefficients, we can only say that the bounded-degree polynomial calculus is at most as powerful as bounded variable infinitary counting logic, but a precise logical characterisation of its power remains an open problem. These connections between logics and proof systems allow us to establish finite-model-theoretic tools for proving lower bounds for the polynomial calculus over the rationals and also over finite fields. This is a corrected version of the paper (arXiv:1802.09377) published originally on January 23, 2019.

In the past decades for more and more graph classes the Graph Isomorphism Problem was shown to be solvable in polynomial time. An interesting family of graph classes arises from intersection graphs of geometric objects. In this work we show that the Graph Isomorphism Problem for unit square graphs, intersection graphs of axis-parallel unit squares in the plane, can be solved in polynomial time. Since the recognition problem for this class of graphs is NP-hard we can not rely on standard techniques for geometric graphs based on constructing a canonical realization. Instead, we develop new techniques which combine structural insights into the class of unit square graphs with understanding of the automorphism group of such graphs. For the latter we introduce a generalization of bounded degree graphs which is used to capture the main structure of unit square graphs. Using group theoretic algorithms we obtain sufficient information to solve the isomorphism problem for unit square graphs.