Asymptotically Smaller Encodings for Graph Problems and Scheduling

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 / |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 Erdos, 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| |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 T), where N is the number of tasks, T the total timespan, and M the number of machines.

Tasks

Reproductions