Asymptotically Smaller Encodings for Graph Problems and Scheduling

TL;DR

This paper introduces more compact CNF encodings for graph problems and scheduling, reducing the number of clauses significantly and enabling more efficient problem-solving and preprocessing techniques.

Contribution

It presents novel encoding methods that drastically reduce the size of CNF representations for graph problems and scheduling, leveraging biclique coverings and dense interval graph properties.

Findings

Graph problem encodings reduced to O(|V|^2 / log |V|) clauses.

New encoding for dense interval graphs uses only O(|V| log |V|) clauses.

Scheduling encoding size decreased from O(NMT^2) to O(NMT + M T^2 log T).

Abstract

We show how several graph problems (e.g., vertex-cover, independent-set, $k$-coloring) can be encoded into CNF using only $O(|V|^2 / \lg |V|)$ many clauses, as opposed to the $\Omega(|V|^2)$ constraints used by standard encodings. This somewhat surprising result is a simple consequence of a result of Erd\H{o}s, Chung, and Spencer (1983) about biclique coverings of graphs, and opens theoretical avenues to understand the success of "Bounded Variable Addition'' (Manthey, Heule, and Biere, 2012) as a preprocessing tool. Finally, we show a novel encoding for independent sets in some dense interval graphs using only $O(|V| \lg |V|)$ clauses (the direct encoding uses $\Omega(|V|^2)$), which we have successfully applied to a string-compression encoding posed by Bannai et al. (2022). As a direct byproduct, we obtain a reduction in the encoding size of a scheduling problem posed by Mayank and Modal (2020) from $O(NMT^2)$ to $O(NMT + M T^2 \lg T)$, where $N$ is the number of tasks, $T$ the total timespan, and $M$ the number of machines.