SAT complexity results from blowing up a reasonable number of variables/clauses (very rarely equivalent to others) in the formula to an enormous number of variable assignments (too many to store, and having only three classes, formula true or false or not evaluated so far, that are not useful equivalencies). What disjoint sets are you thinking of tracking?