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?
