Z3: How to handle association or membership?

user_785494 0
Viewed 69

I'm interested in solving scheduling problems in Z3, which require things like:

  • There are multiple classes: C1, C2, C3...
  • and multiple students: S1, S2, S3...
  • each student needs to be in exactly one class
  • each class needs to have no more than K students

I think of these as sets, but they could be thought of as associations, 2-adic functions (isin(student, class), 1-adic functions (class1(student), student1(class)), bitvectors, arrays...

What is the simplest, easiest way to model these in Z3 and solve problems about them?

smt z3 set
1 Answers

The obvious thing to do would be to do an Array, from custom sorts you've declared (as enumerations) for your classes and students. The array would map these to booleans, giving you membership.

However, note that it's hard for an SMT solver to beat a custom-scheduling algorithm; in case you have an excessive number of constraints and especially if you're also trying to maximize/minimize some sort of a cost function. Having said that, these sorts of things have been done before. Here're two examples:

(On a side note.. Stack-overflow works the best if you try something and run into issues; posting the code you tried. These sorts of "general" guidance questions, unfortunately, aren't the best for this forum. See here: https://stackoverflow.com/help/how-to-ask)

user_9363100
Related