arXiv subjects

Anuj Dawar

Publications and source records attributed to Anuj Dawar.

At least 37 records · Page 2Linked to original sources

arXiv2022

Limitations of the Invertible-Map Equivalences

This note draws conclusions that arise by combining two recent papers, by Anuj Dawar, Erich Grädel, and Wied Pakusa, published at ICALP 2019 and by Moritz Lichter, published at LICS 2021. In both papers, the main technical results rely on the combinatorial and algebraic analysis of the invertible-map equivalences $\equiv^\text{IM}_{k,Q}$ on certain variants of Cai-Fürer-Immerman (CFI) structures. These $\equiv^\text{IM}_{k,Q}$-equivalences, for a number $k$ and a set of primes~$Q$, refine the well-known Weisfeiler-Leman equivalences used in algorithms for graph isomorphism. The intuition is that two graphs $G\equiv^\text{IM}_{k,Q}H$ cannot be distinguished by iterative refinements of equivalences on $k$-tuples defined via linear operators on vector spaces over fields of characteristic $p \in Q$. In the first paper it has been shown, using considerable algebraic machinery, that for a prime $q \notin Q$, the $\equiv^\text{IM}_{k,Q}$ equivalences do not distinguish between non-isomorphic CFI-structures over the field $\mathbb{F}_q$. In the second paper, a similar but not identical construction for CFI-structures over the rings $\mathbb{Z}_{2^i}$ has, again by rather involved combinatorial and algebraic arguments, been shown to be indistinguishable with respect to $\equiv^\text{IM}_{k,\{2\}}$. Together with earlier work, this second result separates rank logic from polynomial time. We unify the two approaches and prove that CFI-structures over the rings $\mathbb{Z}_{2^i}$ are indistinguishable with respect to $\equiv^\text{IM}_{k,\mathbb{P}}$, for the set $\mathbb{P}$ of all primes. This implies the following two results. 1. There is no fixed $k$ such that the invertible-map equivalence $\equiv^\text{IM}_{k,\mathbb{P}}$ coincides with isomorphism on all finite graphs. 2. No extension of fixed-point logic by linear-algebraic operators over fields can capture polynomial time.

cs.LO↗

arXiv2021

Separating LREC from LFP

LREC= is an extension of first-order logic with a logarithmic recursion operator. It was introduced by Grohe et al. and shown to capture the complexity class L over trees and interval graphs. It does not capture L in general as it is contained in FPC - fixed-point logic with counting. We show that this containment is strict. In particular, we show that the path systems problem, a classic P-complete problem which is definable in LFP - fixed-point logic - is not definable in LREC= This shows that the logarithmic recursion mechanism is provably weaker than general least fixed points. The proof is based on a novel Spoiler-Duplicator game tailored for this logic.

cs.LO↗

arXiv2021

Lovász-Type Theorems and Game Comonads

Lovász (1967) showed that two finite relational structures A and B are isomorphic if, and only if, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B for any finite structure C. Soon after, Pultr (1973) proved a categorical generalisation of this fact. We propose a new categorical formulation, which applies to any locally finite category with pushouts and a proper factorisation system. As special cases of this general theorem, we obtain two variants of Lovász' theorem: the result by Dvořák (2010) that characterises equivalence of graphs in the k-dimensional Weisfeiler-Leman equivalence by homomorphism counts from graphs of tree-width at most k, and the result of Grohe (2020) characterising equivalence with respect to first-order logic with counting and quantifier depth k in terms of homomorphism counts from graphs of tree-depth at most k. The connection of our categorical formulation with these results is obtained by means of the game comonads of Abramsky et al. We also present a novel application to homomorphism counts in modal logic.

cs.LO↗

arXiv2021

On the relative power of algebraic approximations of graph isomorphism

We compare the capabilities of two approaches to approximating graph isomorphism using linear algebraic methods: the \emph{invertible map tests} (introduced by Dawar and Holm) and proof systems with algebraic rules, namely \emph{polynomial calculus}, \emph{monomial calculus} and \emph{Nullstellensatz calculus}. In the case of fields of characteristic zero, these variants are all essentially equivalent to the the Weisfeiler-Leman algorithms. In positive characteristic we show that the invertible map method can simulate the monomial calculus and identify a potential way to extend this to the monomial calculus.

cs.LO↗

arXiv2020

Extension Preservation in the Finite and Prefix Classes of First Order Logic

It is well known that the classic Łoś-Tarski preservation theorem fails in the finite: there are first-order definable classes of finite structures closed under extensions which are not definable (in the finite) in the existential fragment of first-order logic. We strengthen this by constructing for every $n$, first-order definable classes of finite structures closed under extensions which are not definable with $n$ quantifier alternations. The classes we construct are definable in the extension of Datalog with negation and indeed in the existential fragment of transitive-closure logic. This answers negatively an open question posed by Rosen and Weinstein.

cs.LO↗

arXiv2020

Symmetric Circuits for Rank Logic

Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finite field. The expressive power of FPR properly extends that of FPC and is contained in PTime, but not known to be properly contained. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by [Anderson and Dawar 2017]. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i.e., invariant under all permutations of their inputs). In the case of FPC, the proof of equivalence of circuits and logic rests heavily on the assumption that individual gates compute such symmetric functions and so novel techniques are required to make this work for FPR.

cs.CC↗

arXiv2020

Generalizations of $k$-Weisfeiler-Leman stabilization

The family of Weisfeiler-Leman equivalences on graphs is a widely studied approximation of graph isomorphism with many different characterizations. We study these, and other approximations of isomorphism defined in terms of refinement operators and Schurian Polynomial Approximation Schemes (SPAS). The general framework of SPAS allows us to study a number of parameters of the refinement operators based on Weisfeiler-Leman refinement, logic with counting, lifts of Weisfeiler-Leman as defined by Evdokimov and Ponomarenko, and the invertible map test introduced by Dawar and Holm, and variations of these, and establish relationships between them.

math.CO↗

arXiv2020

Relativization of Gurevich's Conjectures

Gurevich (1988) conjectured that there is no logic for $\textsf{P}$ or for $\textsf{NP}\cap \textsf{coNP}$. For the latter complexity class, he also showed that the existence of a logic would imply that $\textsf{NP} \cap \textsf{coNP}$ has a complete problem under polynomial time reductions. We show that there is an oracle with respect to which $\textsf P$ does have a logic and $\textsf P \ne\textsf{NP}$. We also show that a logic for $\textsf{NP} \cap \textsf{coNP}$ follows from the existence of a complete problem and a further assumption about canonical labelling. For intersection classes $Σ^p_n \cap Π^p_n$ higher in the polynomial hierarchy, the existence of a logic is equivalent to the existence of complete problems.

cs.LO↗

arXiv2019

Definable Inapproximability: New Challenges for Duplicator

We consider the hardness of approximation of optimization problems from the point of view of definability. For many NP-hard optimization problems it is known that, unless P = NP, no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances.

cs.LO↗

arXiv2019

Approximations of Isomorphism and Logics with Linear-Algebraic Operators

Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parametrised by a number k and a set Q of primes. The intuition is that two graphs G and H which are equivalent with respect to k-Q-IM-equivalence cannot be distinguished by a refinement of k-tuples given by linear operators acting on vector spaces over fields of characteristic p, for any p in Q. These equivalences first appeared in the study of rank logic, but in fact they can be used to delimit the expressive power of any extension of fixed-point logic with linear-algebraic operators. We define an infinitary logic with k variables and all linear-algebraic operators over finite vector spaces of characteristic p in Q and show that the k-Q-IM-equivalence is the natural notion of elementary equivalence for this logic. By means of a new and much deeper algebraic analysis of a generalized variant, for any prime p, of the CFI-structures due to Cai, Fürer, and Immerman, we prove that, as long as Q is not the set of all primes, there is no k such that k-Q-IM-equivalence is the same as isomorphism. It follows that there are polynomial-time properties of graphs which are not definable in the infinitary logic with all Q-linear-algebraic operators and finitely many variables, which implies that no extension of fixed-point logic with linear-algebraic operators can capture PTIME, unless it includes such operators for all prime characteristics. Our analysis requires substantial algebraic machinery, including a homogeneity property of CFI-structures and Maschke's Theorem, an important result from the representation theory of finite groups.

cs.LO↗

arXiv2019

Logical properties of random graphs from small addable classes

We establish zero-one laws and convergence laws for monadic second-order logic (MSO) (and, a fortiori, first-order logic) on a number of interesting graph classes. In particular, we show that MSO obeys a zero-one law on the class of connected planar graphs, the class of connected graphs of tree-width at most $k$ and the class of connected graphs excluding the $k$-clique as a minor. In each of these cases, dropping the connectivity requirement leads to a class where the zero-one law fails but a convergence law for MSO still holds.

cs.LO↗

arXiv2019

Constructing Hard Examples for Graph Isomorphism

We describe a method for generating graphs that provide difficult examples for practical Graph Isomorphism testers. We first give the theoretical construction, showing that we can have a family of graphs without any non-trivial automorphisms which also have high Weisfeiler-Leman dimension. The construction is based on properties of random 3XOR-formulas. We describe how to convert such a formula into a graph which has the desired properties with high probability. We validate the method by an experimental implementation. We construct random formulas and validate them with a SAT solver to filter through suitable ones, and then convert them into graphs. Experimental results demonstrate that the resulting graphs do provide hard examples that match the hardest known benchmarks for graph isomorphism.

cs.CC↗

arXiv2019

On the Power of Symmetric Linear Programs

We consider families of symmetric linear programs (LPs) that decide a property of graphs (or other relational structures) in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates the integer points corresponding to graphs with the property from those corresponding to graphs without the property. We show that this is equivalent, with at most polynomial blow-up in size, to families of symmetric Boolean circuits with threshold gates. In particular, when we consider polynomial-size LPs, the model is equivalent to definability in a non-uniform version of fixed-point logic with counting (FPC). Known upper and lower bounds for FPC apply to the non-uniform version. In particular, this implies that the class of graphs with perfect matchings has polynomial-size symmetric LPs while we obtain an exponential lower bound for symmetric LPs for the class of Hamiltonian graphs. We compare and contrast this with previous results (Yannakakis 1991) showing that any symmetric LPs for the matching and TSP polytopes have exponential size. As an application, we establish that for random, uniformly distributed graphs, polynomial-size symmetric LPs are as powerful as general Boolean circuits. We illustrate the effect of this on the well-studied planted-clique problem.

cs.LO↗

arXiv2017

Bounded degree and planar spectra

The finite spectrum of a first-order sentence is the set of positive integers that are the sizes of its models. The class of finite spectra is known to be the same as the complexity class NE. We consider the spectra obtained by limiting models to be either planar (in the graph-theoretic sense) or by bounding the degree of elements. We show that the class of such spectra is still surprisingly rich by establishing that significant fragments of NE are included among them. At the same time, we establish non-trivial upper bounds showing that not all sets in NE are obtained as planar or bounded-degree spectra.

cs.LO↗

arXiv2017

The pebbling comonad in finite model theory

Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: - Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. - Symmetric games corresponding to equivalence in full k-variable logic are also characterized. - The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. - Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Fürer-Immerman construction. - The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.

cs.LO↗

arXiv2016

Lasserre Lower Bounds and Definability of Semidefinite Programming

For a large class of optimization problems, namely those that can be expressed as finite-valued constraint satisfaction problems (VCSPs), we establish a dichotomy on the number of levels of the Lasserre hierarchy of semi-definite programs (SDPs) that are required to solve the problem exactly. In particular, we show that if a finite-valued constraint problem is not solved exactly by its basic linear programming relaxation, it is also not solved exactly by any sub-linear number of levels of the Lasserre hierarchy. The lower bounds are established through logical undefinability results. We show that the linear programming relaxation of the problem, as well as the SDP corresponding to any fixed level of the Lasserre hierarchy is interpretable in a VCSP instance by means of formulas of fixed-point logic with counting. We also show that the solution of an SDP can be expressed in this logic. Together, these results give a way of translating lower bounds on the number of variables required in counting logic to express a VCSP into lower bounds on the number of levels required in the Lasserre hierarchy to eliminate the integrality gap. As a special case, we obtain the same dichotomy for the class of MAXCSP problems, generalizing some earlier Lasserre lower bound results of Schoenebeck.

cs.LO↗

arXiv2016

Descriptive complexity of graph spectra

Two graphs are co-spectral if their respective adjacency matrices have the same multi-set of eigenvalues. A graph is said to be determined by its spectrum if all graphs that are co-spectral with it are isomorphic to it. We consider these properties in relation to logical definability. We show that any pair of graphs that are elementarily equivalent with respect to the three-variable counting first-order logic $C^3$ are co-spectral, and this is not the case with $C^2$, nor with any number of variables if we exclude counting quantifiers. We also show that the class of graphs that are determined by their spectra is definable in partial fixed-point logic with counting. We relate these properties to other algebraic and combinatorial problems.

cs.LO↗

arXiv2015

A Definability Dichotomy for Finite Valued CSPs

Finite valued constraint satisfaction problems are a formalism for describing many natural optimization problems, where constraints on the values that variables can take come with rational weights and the aim is to find an assignment of minimal cost. Thapper and Zivny have recently established a complexity dichotomy for finite valued constraint languages. They show that each such language either gives rise to a polynomial-time solvable optimization problem, or to an NP-hard one, and establish a criterion to distinguish the two cases. We refine the dichotomy by showing that all optimization problems in the first class are definable in fixed-point language with counting, while all languages in the second class are not definable, even in infinitary logic with counting. Our definability dichotomy is not conditional on any complexity-theoretic assumption.

cs.LO↗