Geometric Graph Representations via Compact SAT Encodings
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(n2d) variables and O(n3d) 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≥3 and n≥2k+1 contains an induced Desargues graph. The resulting lower bound, together with an explicit three-dimensional representation of K(7,3), establishes boxicity(K(7,3))=3. This disproves the conjecture of Caoduro and Sebo that boxicity(K(n,k))=n−k for all k≥3 and n≥2k+1.
Related
- A geometric construction of supercuspidal representations
- Descriptor representations of geometric port-Hamiltonian systems on Hilbert spaces
- Sigmoid Tensor Decomposition for Compact Representations of Binary Data
- Non-unitarizable representations of compact and discrete quantum groups
- Nonlinear Maps Between Irreducible Representations in Graph Neural Networks
BibTeX
@misc{chandran2026geometric,
title = {{Geometric Graph Representations via Compact SAT Encodings}},
author = {L. Sunil Chandran and Rishikesh Gajjala and Suraj Kumar Sahoo and Aatman Supkar},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.22241},
eprint = {2610.22241},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.22241},
}
RIS
TY - UNPB
TI - Geometric Graph Representations via Compact SAT Encodings
AU - L. Sunil Chandran
AU - Rishikesh Gajjala
AU - Suraj Kumar Sahoo
AU - Aatman Supkar
PY - 2026
DA - 2026/10/15
PB - arXiv
DO - 10.48550/arxiv.2610.22241
UR - https://arxiv.org/abs/2610.22241
AB - 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≥3 and n≥2k+1 contains an induced Desargues graph. The resulting lower bound, together with an explicit three-dimensional representation of K(7,3), establishes boxicity(K(7,3))=3. This disproves the conjecture of Caoduro and Sebo that boxicity(K(n,k))=n−k for all k≥3 and n≥2k+1.
ER -