A SAT-based Filtering Framework for Exact Coverings of K33 by Cliques of Order 3, 4 or 5
arXiv:2603.29548
Abstract
We investigate the minimum number of cliques of orders , , and needed to cover the edges of with zero excess. General covering results yield the lower bound 57. The main result of the paper is that no decomposition of into blocks from 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 . A short additional counting argument further strengthens this to . We also give new compressed proofs for the known exceptional cases and in the setting of -decompositions, illustrating the same combination of theoretical reduction and exact computation. Finally, we explain the relevance of the result to the open packing problem of determining the packing number . A packing of copies of in would leave a -regular graph on vertices, and our exclusion already rules out two natural candidate leave structures.