1. A method for determining satisfiability of a bounded model checking instance, comprising: determining reachability of a target control state from an initial control state through a finite set of bounded control paths by: restricting, using a computer processor, decision variable ordering of a satisfiability (SAT) search of a SAT solver stored in computer readable storage media to a sequence of formula variables; and selecting, using the computer processor, a set of control state variables with a higher decision priority than other formula variables in one or more decision paths, each decision path comprising a sequence of Boolean value assignments on unassigned variables.