1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Yuval Filmus Dec 5 '18 at 4:50
  • $\begingroup$ 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? $\endgroup$ – Rachel Dec 5 '18 at 6:19
  • $\begingroup$ 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. $\endgroup$ – Apass.Jack Dec 5 '18 at 7:43
  • $\begingroup$ There are many possible optimizations one could consider. It’s probably not worth it to use all of them, for various reasons, including maintainability. $\endgroup$ – Yuval Filmus Dec 5 '18 at 8:09
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Yeah, I also realized, when I went to ask on their issues page, that pycosat is a general SAT solver. So they would have to do more work to find m for a minimal equisatisfiable 3-SAT formula or something similar. $\endgroup$ – Rachel Dec 7 '18 at 0:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.