Compact SAT methods improve geometric graph dimension finding
Geometric Graph Representations via Compact SAT Encodings
Computational GeometryDiscrete MathematicsData Structures and AlgorithmsLogic in Computer Science
Summary
Determining the geometric dimension in which a graph can be represented by simple shapes like boxes or cubes is a challenging problem. The authors introduce a new way to encode this problem into SAT (logic puzzles that computers solve) much more efficiently than before. Their approach can prove exact answers faster and with certificates that ensure correctness. They also disprove a previous guess about a family of graphs called Kneser graphs, showing one example requires fewer dimensions than expected.
What this means in practice
- •For graph algorithm developers: Efficiently compute exact boxicity and cubicity dimensions for graphs using compact SAT encodings to improve geometric representation tools.
- •For automated reasoning engineers: Use improved SAT encodings and verified certificates to certify exact graph dimension results in formal verification systems.
Authors
L. Sunil Chandran, Rishikesh Gajjala, Suraj Kumar Sahoo, Aatman Supkar
Abstract
We present compact SAT encodings and certifying exact solvers for boxicity and cubicity. The boxicity of a graph is the minimum dimension in which it is the intersection graph of axis-aligned boxes; cubicity is defined analogously using unit cubes. Grid-based formulations face a geometric discretization bottleneck, growing rapidly with the target dimension. We avoid this bottleneck by encoding the total order of interval endpoints in each coordinate. For an $n$-vertex graph and target dimension $d$, our boxicity encoding uses $O(n^2d)$ variables and $O(n^3d)$ clauses, both linear in $d$. Requiring the left- and right-endpoint orders to agree yields a cubicity encoding of the same asymptotic size. Satisfying models are decoded into independently checked geometric representations, while unsatisfiable instances used as lower-bound evidence carry mechanically verified DRAT certificates. In a controlled evaluation with 186 trials per encoding on standard and structured graph families, the order encoding solves 96.8% of trials, compared with 71.0% for the known grid formulation, and reduces mean PAR-2 time from 178.21 to 21.70 seconds. The pipeline also certifies exact values for several named graphs. We turn one such value into a reusable obstruction by proving that every Kneser graph $K(n,k)$ with $k\ge3$ and $n\ge2k+1$ contains an induced Desargues graph. The resulting lower bound, together with an explicit three-dimensional representation of $K(7,3)$, establishes $\operatorname{boxicity}(K(7,3))=3$. This disproves the conjecture of Caoduro and Sebo that $\operatorname{boxicity}(K(n,k))=n-k$ for all $k\ge3$ and $n\ge2k+1$.