arXiv++ Combinatorics

A sweep of a point configuration is any ordered partition induced by a linear functional. Posets of sweeps of planar point configurations were formalized and abstracted by Goodman and Pollack under the theory of allowable sequences of permutations. We introduce two generalizations that model posets of sweeps of higher dimensional configurations. Mimicking the fact that sweep polytopes of point configurations (the monotone path polytopes of the associated zonotopes) are projections of permutahedra, we define sweep oriented matroids as strong maps of the braid oriented matroid. Allowable sequences are then the sweep oriented matroids of rank 2, and many of their properties extend to higher rank. We show strong ties between sweep oriented matroids and both modular hyperplanes and Dilworth truncations from (unoriented) matroid theory. We also explore their connection with the generalized Baues problem for cellular strings, where sweep oriented matroids can play the role of monotone path polytopes, even for non-realizable oriented matroids. In particular, we show that for oriented matroids that admit a sweep oriented matroid, their poset of pseudo-sweeps deformation retracts to a sphere of the appropriate dimension. A second generalization are allowable graphs of permutations: symmetric sets of permutations pairwise connected by allowable sequences. They have the structure of acycloids and include sweep oriented matroids.

We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, which is a community-driven effort to build a unified mathematics library for Lean. One goal of the mathlib project is to contain all of the topics of a complete undergraduate mathematics education. We provide three presentations of the main theorem statement: in terms of indexed families of finite sets, of relations on types, and of matchings in bipartite graphs. We also formalize a version of Kőnig's lemma (in terms of inverse limits) to boost the theorem to the case of countably infinite index sets. We give a description of the design of the recent mathlib library for simple graphs, and we also give a necessary and sufficient condition for a simple graph to carry a function.

We study the problem of detecting the edge correlation between two random graphs with $n$ unlabeled nodes. This is formalized as a hypothesis testing problem, where under the null hypothesis, the two graphs are independently generated; under the alternative, the two graphs are edge-correlated under some latent node correspondence, but have the same marginal distributions as the null. For both Gaussian-weighted complete graphs and dense Erdős-Rényi graphs (with edge probability $n^{-o(1)}$), we determine the sharp threshold at which the optimal testing error probability exhibits a phase transition from zero to one as $n\to \infty$. For sparse Erdős-Rényi graphs with edge probability $n^{-Ω(1)}$, we determine the threshold within a constant factor. The proof of the impossibility results is an application of the conditional second-moment method, where we bound the truncated second moment of the likelihood ratio by carefully conditioning on the typical behavior of the intersection graph (consisting of edges in both observed graphs) and taking into account the cycle structure of the induced random permutation on the edges. Notably, in the sparse regime, this is accomplished by leveraging the pseudoforest structure of subcritical Erdős-Rényi graphs and a careful enumeration of subpseudoforests that can be assembled from short orbits of the edge permutation.

We study a new version of the Traveling Salesperson Problem, called \VectorTSP, where the traveler is subject to discrete acceleration constraints, as defined in the paper-and-pencil game Racetrack (also known as Vector Racer). In this model, the degrees of freedom at a certain point in time depends on the current velocity, and the speed is not limited. The paper introduces this problem and initiates its study, discussing also the main differences with existing versions of TSP. Not surprisingly, the problem turns out to be NP-hard. A key feature of \VectorTSP is that it deals with acceleration in a discrete, combinatorial way, making the problem more amenable to algorithmic investigation. The problem involves two layers of trajectory planning: (1) the order in which cities are visited, and (2) the physical trajectory realizing such a visit, both interacting with each other. This interaction is formalized as an interactive protocol between a high-level tour algorithm and a trajectory oracle, the former calling the latter repeatedly. We present an exact implementation of the trajectory oracle, adapting the A* algorithm for paths over multiple checkpoints whose ordering is \emph{given} (this algorithm being possibly of independent interest). To motivate the problem further, we perform experiments showing that the naive approach consisting of solving the instance as an \EuclideanTSP first, then optimizing the trajectory of the resulting tour, is typically suboptimal and outperformed by simple (but dedicated) heuristics.

An oriented hypergraph is an oriented incidence structure that allows for the generalization of graph theoretic concepts to integer matrices through its locally signed graphic substructure. The locally graphic behaviors are formalized in the subobject classifier of incidence hypergraphs. Moreover, the injective envelope is calculated and shown to contain the class of uniform hypergraphs -- providing a combinatorial framework for the entries of incidence matrices. A multivariable all-minors characteristic polynomial is obtained for both the determinant and permanent of the oriented hypergraphic Laplacian and adjacency matrices arising from any integer incidence matrix. The coefficients of each polynomial are shown to be submonic maps from the same family into the injective envelope limited by the subobject classifier. These results provide a unifying theorem for oriented hypergraphic matrix-tree-type and Sachs-coefficient-type theorems. Finally, by specializing to bidirected graphs, the trivial subclasses for the degree-$k$ monomials of the Laplacian are shown to be in one-to-one correspondence with $k$-arborescences.

The topic of this paper is "gerrymandering", namely the curse of deliberate creations of district maps with highly asymmetric electoral outcomes to disenfranchise voters, and it has a long legal history. Measuring and eliminating gerrymandering has enormous implications to sustain the backbone of democratic principles of a society. Although there is no dearth of legal briefs involving gerrymandering over many years, it is only more recently that mathematicians and applied computational researchers have started to investigate this topic. However, it has received relatively little attention so far from the computational complexity researchers dealing with theoretical analysis of computational complexity issues, such as computational hardness, approximability issues, etc. There could be many reasons for this, such as descriptions of these problem non-CS non-math (often legal or political) journals that theoretical CS (TCS) people usually do not follow, or the lack of coverage of these topics in TCS publication venues. One of our modest goals in writing this article is to improve upon this situation by stimulating further interactions between the gerrymandering and TCS researchers. To this effect, our main contributions are twofold: (1) we provide formalization of several models, related concepts, and corresponding problem statements using TCS frameworks from the descriptions of these problems as available in existing non-TCS (perhaps legal) venues, and (2) we also provide computational complexity analysis of some versions of these problems, leaving other versions for future research. The goal of writing this article is not to have the final word on gerrymandering, but to introduce a series of concepts, models and problems to the TCS community and to show that science of gerrymandering involves an intriguing set of partitioning problems involving geometric and combinatorial optimization.

Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling, automated theorem provers for first-order logic, SAT/SMT solvers aimed at program verification, and higher-order proof assistants for checking mathematical proofs. More recently, some of these lines of research have started to converge in complementary ways. One success story is the combination of SAT solvers and CASs (SAT+CAS) aimed at resolving mathematical conjectures. Many conjectures in pure and applied mathematics are not amenable to traditional proof methods. Instead, they are best addressed via computational methods that involve very large combinatorial search spaces. SAT solvers are powerful methods to search through such large combinatorial spaces---consequently, many problems from a variety of mathematical domains have been reduced to SAT in an attempt to resolve them. However, solvers traditionally lack deep repositories of mathematical domain knowledge that can be crucial to pruning such large search spaces. By contrast, CASs are deep repositories of mathematical knowledge but lack efficient general search capabilities. By combining the search power of SAT with the deep mathematical knowledge in CASs we can solve many problems in mathematics that no other known methods seem capable of solving. We demonstrate the success of the SAT+CAS paradigm by highlighting many conjectures that have been disproven, verified, or partially verified using our tool MathCheck. These successes indicate that the paradigm is positioned to become a standard method for solving problems requiring both a significant amount of search and deep mathematical reasoning. For example, the SAT+CAS paradigm has recently been used by Heule, Kauers, and Seidl to find many new algorithms for $3\times3$ matrix multiplication.

In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly known as the \emph{cap set problem}. Ellenberg and Gijswijt's proof was published in the \emph{Annals of Mathematics} and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in $\mathbb{F}^n_q$ and concrete values for the case $q = 3$. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.

According to Walter M. Fitch, two genes are xenologs if they are separated by at least one horizontal gene transfer. This concept is formalized through Fitch relations, which are defined as binary relations that comprise all pairs $(x,y)$ of genes $x$ and $y$ for which $y$ has been horizontally transferred at least once since it diverged from the least common ancestor of $x$ and $y$. This definition, in particular, preserves the directional character of the transfer. Fitch relations are characterized by a small set of forbidden induced subgraphs on three vertices and can be recognized in linear time. In this contribution, we provide two novel characterizations of Fitch relations and present an alternative, short and elegant proof of the characterization theorem established by Geiß et al.\ in \emph{J.\ Math.\ Bio 77(5), 2018}.

The shuffle product has a connection with several useful permutation statistics such as descent and peak, and corresponds to the multiplication operation in the corresponding descent and peak algebras. In their recent work, Gessel and Zhuang formalized the notion of shuffle-compatibility and studied various permutation statistics from this viewpoint. They further conjectured that any shuffle compatible permutation statistic is a descent statistic. In this note we construct a counter-example to this conjecture.

We study Ramsey's theorem for pairs and two colours in the context of the theory of $α$-large sets introduced by Ketonen and Solovay. We prove that any $2$-colouring of pairs from an $ω^{300n}$-large set admits an $ω^n$-large homogeneous set. We explain how a formalized version of this bound gives a more direct proof, and a strengthening, of the recent result of Patey and Yokoyama [Adv. Math. 330 (2018), 1034--1070] stating that Ramsey's theorem for pairs and two colours is $\forallΣ^0_2$-conservative over the axiomatic theory $\mathsf{RCA}_0$ (recursive comprehension).

The switch Markov chain has been extensively studied as the most natural Markov Chain Monte Carlo approach for sampling graphs with prescribed degree sequences. We use comparison arguments with other, less natural but simpler to analyze, Markov chains, to show that the switch chain mixes rapidly in two different settings. We first study the classic problem of uniformly sampling simple undirected, as well as bipartite, graphs with a given degree sequence. We apply an embedding argument, involving a Markov chain defined by Jerrum and Sinclair (TCS, 1990) for sampling graphs that almost have a given degree sequence, to show rapid mixing for degree sequences satisfying strong stability, a notion closely related to $P$-stability. This results in a much shorter proof that unifies the currently known rapid mixing results of the switch chain and extends them up to sharp characterizations of $P$-stability. In particular, our work resolves an open problem posed by Greenhill (SODA, 2015). Secondly, in order to illustrate the power of our approach, we study the problem of uniformly sampling graphs for which, in addition to the degree sequence, a joint degree distribution is given. Although the problem was formalized over a decade ago, and despite its practical significance in generating synthetic network topologies, small progress has been made on the random sampling of such graphs. The case of a single degree class reduces to sampling of regular graphs, but beyond this almost nothing is known. We fully resolve the case of two degree classes, by showing that the switch Markov chain is always rapidly mixing. Again, we first analyze an auxiliary chain for strongly stable instances on an augmented state space and then use an embedding argument.

Over an alphabet of size 3 we construct an infinite balanced word with critical exponent 2+sqrt(2)/2. Over an alphabet of size 4 we construct an infinite balanced word with critical exponent (5+sqrt(5))/4. Over larger alphabets, we give some candidates for balanced words (found computationally) having small critical exponents. We also explore a method for proving these results using the automated theorem prover Walnut.

We study the famous mathematical puzzle of prisoners and hats. We introduce a framework in which various variants of the problem can be formalized. We examine three particular versions of the problem (each one in fact a class of problems) and completely characterize them as to (non)existence of winning strategies.

The notions of symmetry and anonymity in strategic games have been formalized in different ways in the literature. We propose a combinatorial framework to analyze these notions, using group actions. Then, the same framework is used to define partial symmetries in payoff matrices. With this purpose, we introduce the notion of the role a player plays with respect to another one, and combinatorial relations between roles are studied. Building on them, we define relations directly between players, which provide yet another characterization of structural symmetries in the payoff matrices of strategic games.

We show that in the random hyperbolic graph model as formalized by Gugelmann et al. in the most interesting range of $\frac12 < α< 1$ the size of the second largest component is $Θ((\log n)^{1/(1-α)})$, thus answering a question of Bode et al. We also show that for $α=\frac12$ with constant probability the corresponding size is $Θ(\log n)$, whereas for $α=1$ it is $Ω(n^{b})$ for some $b > 0$.

We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define the basic predicates over polyhedra in an effective way (i.e., as programs), and relate them with the corresponding usual logical counterparts. To this end, we make an extensive use of the Boolean reflection methodology. The benefit of this approach is that we can easily derive the proof of several fundamental results on polyhedra, such as Farkas' Lemma, the duality theorem of linear programming, and Minkowski's Theorem.

We present 35 open problems on combinatorial, geometric and algebraic aspects of k-orbit abstract polytopes. We also present a theory of rooted polytopes that has appeared implicitly in previous work but has not been formalized before.

This paper describes an enumeration of all words having a combinatoric property called "rhythmic oddity property"named \emph{rop-words}.\ This property was introduced by Simha Aron in the 1990s. The set of rop-words is not a subset of the set of Lyndon words, but is very closed. We show that there is a bijection between some necklaces and rop-words. This leads to a formula for counting the rop-words of a given length. \textsc{Keywords:} Combinatoric on words. Lyndon words. Rhythmic oddity. Music formalization

We develop new methods based on graph motifs for graph clustering, allowing more efficient detection of communities within networks. We focus on triangles within graphs, but our techniques extend to other clique motifs as well. Our intuition, which has been suggested but not formalized similarly in previous works, is that triangles are a better signature of community than edges. We therefore generalize the notion of conductance for a graph to {\em triangle conductance}, where the edges are weighted according to the number of triangles containing the edge. This methodology allows us to develop variations of several existing clustering techniques, including spectral clustering, that minimize triangles split by the cluster instead of edges cut by the cluster. We provide theoretical results in a planted partition model to demonstrate the potential for triangle conductance in clustering problems. We then show experimentally the effectiveness of our methods to multiple applications in machine learning and graph mining.