1. A method of multi-target Boolean Satisfiability (SAT)-based pattern generation, comprising: receiving circuit design information for a circuit and a set of faults that model a plurality of potential defects in the circuit; constructing a SAT instance based on the circuit design information and the set of faults; applying a SAT solving engine to the SAT instance; and outputting a test pattern based on an satisfying assignment derived from solving the SAT instance or a report that a test pattern cannot be generated.