1

I am trying to model job shop scheduling problems using Z3. Specifically let's say i have a set of tasks each of which may have other task dependencies. Then I wish to minimize the time of scheduling the last tasks i.e. the makespan.

Since there can be more than one job which has dependencies on other jobs but no forward dependencies (i.e. no job depends on this one), A simple minimize operation in Z3 may not suffice. And Z3 doesn't admit to a max function over a list.

Hence to solve this, I am considering adding a fake job which depends on all such jobs and then minimizing the time of scheduling this job. I wonder if this approach is scalable as I need to add constraints to many jobs.

Is this the only approach or are there other more elegant means?

Ruby Spring
  • 11
  • 1
  • 1
    Could you add a concrete example of the problem you are trying to solve? In particular, is the number of jobs known at query time? – James Wilcox Sep 13 '17 at 04:33

1 Answers1

0

You can define max using a chain of ite calls yourself; assuming you know exactly how many jobs there are. See here: Use Z3 and SMT-LIB to get a maximum of two values

alias
  • 28,120
  • 2
  • 23
  • 40