I don't really have an answer for you, but there are at least some easy simplifications you can perform:

(1) If both occurrences of a variable have the same sign (or a variable occurs only once), you might as well set it to the value that makes both occurrences true.

(2) Suppose that both occurrences of a variable have opposite signs, and the paths from them to their least common ancestor in the expression tree consists only of conjunctions. Then all the values at the intermediate expressions along one of these paths, and at the LCA, must be false, so you might as well replace that whole subtree by a false literal.

(3) Added after seeing Ryan's example of (x y) ¬x ¬y: suppose that both occurrences of a variable have opposite signs, and one of the paths to their least common ancestor consists only of conjunctions. Then you might as well set that occurrence of the variable to be true, and the other one to false, because the opposite setting cannot lead to a true value at the LCA.

Maybe it's the case that any nontrivial formula containing neither none of these patterns is always satisfiable?

Post Undeleted by David Eppstein
2 added 328 characters in body

I don't really have an answer for you, but there are at least some easy simplifications you can perform:

(1) If both occurrences of a variable occurs at most twice in a CNF formulahave the same sign, then you might as well set it can be eliminated by resolution forming to the value that makes both occurrences true.

(2) Suppose that both occurrences of a CNF formula with one fewer clausevariable have opposite signs, and without increasing the number of occurrences of paths from them to their least common ancestor in the other variablesexpression tree consists only of conjunctions. Therefore, if Then all variables occur the values at most twicethe intermediate expressions along one of these paths, resolution will solve and at the problem in polynomial timeLCA, must be false, so you might as well replace that whole subtree by a false literal.

Maybe it's the case that any nontrivial formula containing neither of these patterns is always satisfiable?

Post Deleted by David Eppstein
1