A SAT-based Filtering Framework for Exact Coverings of K33 by Cliques of Order 3, 4 or 5

TL;DR

This paper develops an algorithmic SAT-based framework to prove the non-existence of certain clique coverings of K33, improving computational methods for combinatorial design problems.

Contribution

It introduces a layered exact-search pipeline combining symmetry reduction, local signatures, and SAT solving, outperforming traditional ILP and DLX methods.

Findings

No decomposition of K33 into 57 K3, K4, K5 blocks exists.

Established lower bounds C^ξ(33,{3,4,5},2) ≥ 58 and ≥ 59.

Provided new proofs for K18 and K19 decompositions.

Abstract

We investigate the minimum number of cliques of orders $3$, $4$, and $5$ needed to cover the edges of $K_{33}$ with zero excess. General covering results yield the lower bound 57. The main result of the paper is that no decomposition of $K_{33}$ into $57$ blocks from $\{K_3,K_4,K_5\}$ exists. Our approach is algorithmic and relies on a layered exact-search pipeline rather than a single monolithic solver. We combine symmetry reduction, enumeration of local signatures, arithmetic profile restrictions, geometric tests for partial configurations, SAT realisation on reduced instances, and final decoding checks. The benchmark comparison shows that this structured approach is substantially more effective than direct ILP, DLX, or SAT formulations on the full problem. As a consequence, we obtain $C^\xi(33,\{3,4,5\},2)\ge 58$. A short additional counting argument further strengthens this to $C^\xi(33,\{3,4,5\},2)\ge 59$. We also give new compressed proofs for the known exceptional cases $K_{18}$ and $K_{19}$ in the setting of $\{K_3,K_4\}$-decompositions, illustrating the same combination of theoretical reduction and exact computation. Finally, we explain the relevance of the $K_{33}$ result to the open packing problem of determining the packing number $D(33,5,2)$. A packing of $51$ copies of $K_5$ in $K_{33}$ would leave a $4$-regular graph on $9$ vertices, and our exclusion already rules out two natural candidate leave structures.