We define a general framework of partition games for formulating two-player pebble games over finite structures. We show that one particular such game, which we call the invertible-map game, yields a family of polynomial-time approximations of graph isomorphism that is strictly stronger than the well-known Weisfeiler-Lehman method. The general framework we introduce includes as special cases the pebble games for finite-variable logics with and without counting. It also includes a matrix-equivalence game, introduced here, which characterises equivalence in the finite-variable fragments of matrix-rank logic. We show that the equivalence defined by the invertible-map game is a refinement of the equivalence defined by each of these games for finite-variable logics.

We show that the ellipsoid method for solving linear programs can be implemented in a way that respects the symmetry of the program being solved. That is to say, there is an algorithmic implementation of the method that does not distinguish, or make choices, between variables or constraints in the program unless they are distinguished by properties definable from the program. In particular, we demonstrate that the solvability of linear programs can be expressed in fixed-point logic with counting (FPC) as long as the program is given by a separation oracle that is itself definable in FPC. We use this to show that the size of a maximum matching in a graph is definable in FPC. This settles an open problem first posed by Blass, Gurevich and Shelah [Blass et al. 1999]. On the way to defining a suitable separation oracle for the maximum matching program, we provide FPC formulas defining canonical maximum flows and minimum cuts in undirected capacitated graphs.

We establish the expressibility in fixed-point logic with counting (FPC) of a number of natural polynomial-time problems. In particular, we show that the size of a maximum matching in a graph is definable in FPC. This settles an open problem first posed by Blass, Gurevich and Shelah [1], who asked whether the existence of perfect matchings in general graphs could be determined in the more powerful formalism of choiceless polynomial time with counting. Our result is established by noting that the ellipsoid method for solving linear programs of full dimension can be implemented in FPC. This allows us to prove that linear programs of full dimension can be optimised in FPC if the corresponding separation oracle problem can be defined in FPC. On the way to defining a suitable separation oracle for the maximum matching problem, we provide FPC formulas defining maximum flows and canonical minimum cuts in capacitated graphs.

We introduce extensions of first-order logic (FO) and fixed-point logic (FP) with operators that compute the rank of a definable matrix. These operators are generalizations of the counting operations in FP+C (i.e. fixed-point logic with counting) that allow us to count the dimension of a definable vector space, rather than just count the cardinality of a definable set. The logics we define have data complexity contained in polynomial time and all known examples of polynomial time queries that are not definable in FP+C are definable in FP+rk, the extension of FP with rank operators. For each prime number p and each positive integer n, we have rank operators rkpfor determining the rank of a matrix over the finite field GFpdefined by a formula over n-tuples. We compare the expressive power of the logics obtained by varying the values p and n can take. In particular, we show that increasing the arity of the operators yields an infinite hierarchy of expressive power. The rank operators are surprisingly expressive, even in the absence of fixed-point operators. We show that FO+rkpcan define deterministic and symmetric transitive closure. This allows us to show that, on ordered structures, FO+rkpcaptures the complexity class MODpL, for all prime values of p.