Asymptotically Smaller Encodings for Graph Problems and Scheduling

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 ErdHos, 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(NMT2) to O(NMT + M T2 lg T), where N is the number of tasks, T the total timespan, and M the number of machines.