1 ) A method for Boolean Satisfiability (SAT), said method comprising: a) using a variable decision heuristic in a SAT algorithm; and b) pruning the search space of SAT using said decision heuristic, wherein said decision heuristic is based on partitioning a conjunctive normal form (CNF) of a Boolean formula corresponding to the SAT and said partitioning is induced by a separator set.