I just wonder if solving largely monotone SAT formulas (meaning most clauses do not contain negated literals, but some do) is in any way easier than general SAT formulas? In other words, are there heuristics specially designed for solving such formulas that are not applicable to more general SAT problems? I tried but didn't find any research in this particular direction.

Of course, what is considered "most" is up to interpretation, but let's say >95% of the causes are monotone.


The theory probably depends on the details. In practice, if you're only interested in solving an instance, here are a some thoughts:

  • Most literals should be eliminated in presolve of today's solvers. They eliminate all positive-only (or negative-only) literals.
  • Next, your setup implies that most literals should be set to $true$. Many solvers allow you to specify which assignment should be tried first ("initial phase"). By setting this to $true$, you should get fast solves.
  • The potentially exponential blowup from resolution might be avoided, if there are very few negated literals. Thus, BVE and DP-based solvers could be quite effective on such formulas.
  • Local search solvers (WalkSAT & Co) should also do very well.

Have you tried feeding your problem to Kissat or CaDiCaL?

  • 1
    $\begingroup$ I suspect that WalkSAT might be a bit outdated. I've had great results using Sparrow which is a modern stochastic local search solver. $\endgroup$ – Juho Jan 27 at 7:17
  • $\begingroup$ This is helpful. I am gonna try out some of these things soon. $\endgroup$ – apen Feb 1 at 20:18

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.