I have used z3 for a job scheduling problem. I had a piece of equipment which can handle capacity X, jobs come in at known intervals and are available for given

I have used z3 for a job scheduling problem. I had a piece of equipment which can handle capacity X, jobs come in at known intervals and are available for given durations of varying lengths, some jobs come in multiple times, some jobs must be done above all others. Which jobs should be assigned to the equipment to maximize completed jobs while not missing the high priority entries? Numbers were such that you could only ever handle a fraction of the possible work. The throughout of a good allocation could be significantly higher than a naive one.