Solving largely monotone SAT formulas
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?