Integrating SAT with MDG for Efficient Invariant
Checking