Bounded Satisfiability Checking of Metric Temporal Logic Specifications