Boolean Abstraction for Temporal Logic Satisfiability