Asymptotically Smaller Encodings for Graph Problems and Scheduling
This work provides theoretical insights for improving preprocessing in SAT solving, with applications in graph theory and scheduling, but it is incremental as it builds on existing results.
The paper tackles the problem of reducing encoding sizes for graph problems and scheduling by showing that several graph problems can be encoded into CNF with O(|V|^2 / lg |V|) clauses instead of Ω(|V|^2), and it applies this to reduce a scheduling encoding from O(NMT^2) to O(NMT + M T^2 lg T).
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 $Ω(|V|^2)$ constraints used by standard encodings. This somewhat surprising result is a simple consequence of a result of Erdő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 $Ω(|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.