Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Petr Kovař, Yifan Zhang

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^ξ(33,\{3,4,5\},2)\ge 58$. A short additional counting argument further strengthens this to $C^ξ(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.

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

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.

Paper Structure

This paper contains 31 sections, 11 theorems, 47 equations, 1 figure, 8 tables.

Table of Contents

  1. Introduction
  2. Three standard exact paradigms
  3. Integer linear programming (ILP)
  4. Dancing links (DLX)
  5. SAT
  6. A warm-up: $K_{18}$ and $K_{19}$ with block sizes $3$ and $4$
  7. Lower bound for $K_{18}$
  8. Excluding $\alpha=7$.
  9. Excluding $\alpha=9$.
  10. Excluding $\alpha=11$.
  11. Excluding $\alpha=13$.
  12. Lower bound for $K_{19}$
  13. Excluding $\alpha=7$.
  14. Excluding $\alpha=9$.
  15. Excluding $\alpha=11$.
  16. ...and 16 more sections

Key Result

Theorem 1.1

There is no decomposition of $K_{33}$ into $57$ cliques of orders from $\{3, 4, 5\}$.

Figures (1)

  • Figure 1: Comparison of the dancing links (1 solution) with integer linear programming

Theorems & Definitions (16)

  • Theorem 1.1
  • Theorem 1.2
  • Theorem 3.1
  • Theorem 4.1: k3k4k5paper
  • Proposition 4.2: k3k4k5paper
  • Remark 4.3
  • Lemma 6.1
  • proof
  • Theorem 6.2: Whitney_1932Hemminger_1972
  • Lemma 6.3
  • ...and 6 more