# Asymptotically Smaller Encodings for Graph Problems and Scheduling

arXiv: https://arxiv.org/abs/2506.14042 · HTML: https://mlsanity.com/paper/2506.14042/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 34 references that are in the map.
- First posted on arXiv 16 Jun 2025.

## Builds on (most cited first, 6 of 6)

- [Effective Auxiliary Variables via Structured Reencoding](https://mlsanity.com/paper/2307.01904/) (2023)
- [The Packing Chromatic Number of the Infinite Square Grid is 15](https://mlsanity.com/paper/2301.09757/) (2023)
- [Happy Ending: An Empty Hexagon in Every Set of 30 Points](https://mlsanity.com/paper/2403.00737/) (2024)
- [A SAT Approach to Clique-Width](https://mlsanity.com/paper/1304.5498/) (2013)
- [Yet Another Comparison of SAT Encodings for the At-Most-K Constraint](https://mlsanity.com/paper/2005.06274/) (2020)
- [Computing NP-hard Repetitiveness Measures via MAX-SAT](https://mlsanity.com/paper/2207.02571/) (2022)

## Abstract (arXiv)

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.