Why is this SAT problem hard?
A change in perspective may be helpful. It is expected that some SAT problems are extraordinarily hard: if the strong exponential time hypothesis is true, then for any SAT solver $A$, there are some specific formulas $\varphi$ that $A$ takes exponential time on. Plug in $A = \mathsf{glucose}$ or $\mathsf{kissat}$ to this statement, and you have chanced upon one such example $\varphi$. The fact this only occurs in 1 in a million cases is just a testament to how strong SAT solvers have become on average cases.
In fact, it is typically not hard to come up with formulas to stump even the best SAT solvers, and all SAT solver users encounter such formulas sooner or later. In my experience, this often happens when taking a sufficiently "mathematically complex" statement and encoding it as a SAT problem. For example, for a long time, the pigeonhole principle, when encoded directly into SAT, was very difficult for SAT solvers to figure out. (I know there was active research on the pigeonhole case, so it's possible that modern SAT solvers no longer suffer from that particular barrier.)
Regarding the number of variables and clauses: for "hard" instances $\varphi$, the time required to solve will be exponential in the number of variables and clauses. So you can't necessarily expect that just because there are a small number of variables or clauses, the problem will be tractable.
What can I do about it?
This one I have a much more positive answer for! Researchers working on SAT solvers typically love examples like this as they are very interesting case studies for improving their tools. So what you can and should do is:
Post the example publicly (you have already done this, but consider also posting it on, e.g. GitHub or Pastebin)
Share the example with the solvers you have tried as a hard instance, for example by posting an issue or by sending an email to active maintainers. Be sure to explain your use case/application to make the example interesting. You've already formed a more "minimal" instance, which is great as it will help them to isolate the difficulty.
Finally, the other thing you can do is try to leverage your own domain expertise to simplify the problem at formula generation time. As one example of an optimization to try, symmetry breaking can be very useful. That is, find an encoding of your graph theory problem which hardcodes constraints on the solution and avoids sources of exponential blowup in the number of cases to check.
