Detecting Hardware Trojans in Unspecified Functionality Through Solving Satisfiability Problems