Why not do these checks on the number of clauses in 3-SAT?

Question

I've been writing a 3-SAT solver for fun and comparing its performance against the solver pycosat. My solver vastly outperforms pycosat in two special cases, where I solve by doing simple, obvious checks, which pycosat doesn't seem to do (based on the time it takes to solve these cases).

I presumed that these checks would be known and commonly incorporated into solvers. Is that the case? Why would a solver not bother doing them?

The checks are based on the following:

Let $\phi$ be a CNF with $n$ variables and $m$ disjunctions, where each disjunction has exactly 3 distinct variables and no two disjunctions have the same literals.

1) If $m < 8$, then $\phi$ is satisfiable.

2) If $m > 7* \binom{n}{3}$, then $\phi$ is unsatisfiable. ($\binom{n}{k}$ is the binomial coefficient.)

The proof is simple but tedious. I can provide it if needed.

Answer 1

There's no real reason not to do your checks given that they are computationally tractable, but there's very little point in doing them either. Your checks make determining the satisfiability of easy random 3-SAT instances easier. SAT solver authors are interested in algorithms that make hard SAT instances easier.

For random 3-SAT, the hardest instances are known to be near the phase transition point where instances on one side are almost always satisfiable and instances on the other are almost always unsatisfiable. That transition point has been observed empirically to be when the ratio of the number of clauses and the number of variables is around 4.26. Your checks would never be helpful with such instances.