In a monotone CNF formula every clause contains only positive literals or only negative literals. In an intersecting monotone CNF formula every positive clause has some variable in common with every negative clause.

The decision problem

INTERSECTING MONOTONE SAT
Input: intersecting monotone CNF formula $f$
Question: is $f$ satisfiable?

has an $n^{o(\log\ n)}$ algorithm dating back to 1996, but is not known to be in P. (Of course, it might turn out to be in P, but that would be a major result.)

• Thomas Eiter and Georg Gottlob, Hypergraph Transversal Computation and Related Problems in Logic and AI, JELIA 2002. doi: 10.1007/3-540-45757-7_53