Solving largely monotone SAT formulas 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 &quot;most&quot; is up to interpretation, but let's say &gt;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 (&quot;initial phase&quot;). 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 &amp; Co) should also do very well.

Have you tried feeding your problem to Kissat or CaDiCaL?