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

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.

• Presumably, this kind of situation tends not to occur in practice. Furthermore, to the extent that it does occur, perhaps the user will be aware of it, and so avoid calling the solver altogether. Finally, your two examples are probably easy for solvers, so there’s not much to gain. – Yuval Filmus Dec 5 '18 at 4:50
• Sure, maybe the input is rarely seen. However, m is given, and x = 7*n*(n-1)*(n-2)//6 is ~n^3, and basically free to calculate. You check two inequalities once, also basically free. The check time is constant. For some random samples with n=100, m=x+1=1,131,901, pycosat takes ~600 ms on my machine, in line w/ its times for other m. My version w/ the check solves same in ~300 ns. For n=100, m=x, pycosat takes ~600ms, mine (w/out help from check) ~500ms. That's ms vs ns at n=100. Check version solves in ~constant time, no-check version time grows and possibly fails. How is that not much to gain? – Rachel Dec 5 '18 at 6:19
• The best place to discuss this problem is, apparently and of course, at the Issues page of · ContinuumIO/pycosat at github. Unless you cannot get a satisfying answer there, you may want to ask the readers here to chime in. – Apass.Jack Dec 5 '18 at 7:43
• There are many possible optimizations one could consider. It’s probably not worth it to use all of them, for various reasons, including maintainability. – Yuval Filmus Dec 5 '18 at 8:09