Computing infeasibility certificates for combinatorial problems through Hilbert’s Nullstellensatz

Systems of polynomial equations with coefficients over a field KK can be used to concisely model combinatorial problems. In this way, a combinatorial problem is feasible (e.g., a graph is 3-colorable, hamiltonian, etc.) if and only if a related system of polynomial equations has a solution over the algebraic closure of the field KK. In this paper, we investigate an algorithm aimed at proving combinatorial infeasibility based on the observed low degree of Hilbert’s Nullstellensatz certificates for polynomial systems arising in combinatorics, and based on fast large-scale linear-algebra computations over KK. We also describe several mathematical ideas for optimizing our algorithm, such as using alternative forms of the Nullstellensatz for computation, adding carefully constructed polynomials to our system, branching and exploiting symmetry. We report on experiments based on the problem of proving the non-3-colorability of graphs. We successfully solved graph instances with almost two thousand nodes and tens of thousands of edges.

► We model combinatorial problems using structured systems of polynomial equations.
► We give an algorithm for solving such systems based on Hilbert’s Nullstellensatz.
► We solved graph colorability queries with almost 2000 nodes and 10 000 edges.
► The performance is based on small Nullstellensatz certificates and fast linear algebra.
► We explain six mathematical results for future speed up of the algorithm.