We introduce ZykovColor, a novel SATbased algorithm to solve the graph coloring problem working on top of an encoding that mimics the Zykov tree. Our method is based on an approach of Hébrard and Katsirelos (2020) that employs a propagator to enforce transitivity constraints, incorporate lower bounds for search tree pruning, and enable inferred propagations.

Regionalization is a fundamental task in spatial analysis that seeks to partition a larger area - such as a country - into smaller regions that are homogeneous with respect to a given attribute. A popular model for regionalization is the p-regions problem, in which regions are formed by grouping the areas of an input planar subdivision. Given the subdivision’s adjacency graph G and pairwise dissimilarities between vertices, the goal is to partition G into a fixed number p of connected subgraphs, such as to minimize the sum of dissimilarities over all vertex pairs in the same subgraph. The problem is NP-hard and even small instances are difficult to solve to provable optimality. In this paper, we present the new ILP model ER-S for the p-regions problem, exploiting a connection between the p-regions objective and the k-partitioning problem. Furthermore, we strengthen the known ILP model Tree with a new type of subtour elimination inequality specific to the p-regions problem. Combining ER-S and the strengthened version of Tree yields the model ER-S-Tree, which dominates the state-of-the-art models in polyhedral strength. This theoretical advantage is reflected in its superior performance in our experimental evaluation. In particular, the new models ER-S and ER-S-Tree enable the solution of problem instances for major European countries that were previously intractable.

In this paper, we suggest new SAT encodings of the partial-ordering based ILP model for the graph coloring problem (GCP) and the bandwidth coloring problem (BCP). The GCP asks for the minimum number of colors that can be assigned to the vertices of a given graph such that each two adjacent vertices get different colors. The BCP is a generalization, where each edge has a weight that enforces a minimal "distance" between the assigned colors, and the goal is to minimize the "largest" color used. For the widely studied GCP, we experimentally compare our new SAT encoding to the state-of-the-art approaches on the DIMACS benchmark set. Our evaluation confirms that this SAT encoding is effective for sparse graphs and even outperforms the state-of-the-art on some DIMACS instances. For the BCP, our theoretical analysis shows that the partial-ordering based SAT and ILP formulations have an asymptotically smaller size than that of the classical assignment-based model. Our practical evaluation confirms not only a dominance compared to the assignment-based encodings but also to the state-of-the-art approaches on a set of benchmark instances. Up to our knowledge, we have solved several open instances of the BCP from the literature for the first time.