A BMC-Based Formulation for the Scheduling Problem in Highly Constrained Hardware Systems