[anonymousDan]

On a related note, anyone have any advice for getting started with something like Z3?

[sevensor]

It really helps to have a hard problem to solve in the first place. Try scheduling all the classes in a university timetable into available classrooms, subject to constraints like maximum seating and not double booking an instructor. Now try to add constraints like “art classes must be in a studio.” Then to make it really fun, “no more than one fourth of the Electrical Engineering classes may be taught outside of the EE building.”

[mkl]

And even better, consecutive tutorials must be in the same room or nearby rooms (tutors and teaching materials can't teleport), and there are two or three simultaneous sequences of tutorials in big courses (so consecutive tutorials actually can be in distant rooms if they're in different sequences), and the number of students requires that the university's rooms be in use 90% of the time, and medium to large lecture theatres must be in use 98% of the time.

This is an annual battle I engage in. The software sucks.

[sevensor]

It does, but better scheduling will only go so far at an institution that underinvests in classroom space. Between “looks fancy” and “meets instructional needs,” donors prefer to have their names on “looks fancy” every time.

[mkl]

It's a public university, donors are not a significant source of funding, and government funding has not increased commensurately with the number of students, which has gone up dramatically in recent years (mainly due to relative cost of living, so no guarantee it will last).

[adsharma]

I find both z3 native syntax (smt 2, lispish) and z3py hard to use.

Here's an alternative syntax that uses python3 types. Works by transpiling to smt 2.

https://gist.github.com/adsharma/45fbb065a8fe793030e8360daeb...

https://github.com/py2many/py2many/blob/main/tests/cases/dem...

[Jtsummers]

https://theory.stanford.edu/~nikolaj/programmingz3.html - This one was useful for me to get started with it a while ago.

[drdrey]

https://microsoft.github.io/z3guide/docs/logic/intro/

[constructum]

If you want to use Z3 with a .NET language, there is also this very useful file with examples of how to use the bindings:

https://github.com/Z3Prover/z3/blob/master/examples/dotnet/P...

The examples are in C#, but easy to adapt to other languages. I found them quite useful to write a program for symbolic execution in F# that calls Z3 to simplify conditionals, here is its interface to Z3:

https://github.com/constructum/asm-symbolic-execution/blob/m...

The bindings are perhaps a bit cumbersome, but rather easy to understand and work very well. Once you appropriately wrap what you need, you can forget about the bindings as well as avoiding SMT-LIB completely.

[cchianel]

For constraint programming solvers, you need to define a model (i.e. what are the variables that the solver can change). Typically, a good model naturally enforces hard constraints. For instance, consider the employee scheduling problem, where you have a list of shifts that need to be assigned a single employee. Two possible models for it are:

- Use a boolean variable that is true if and only if a particular employee is assigned to a particular shift. For 2 shifts (A, B) and 2 employees (Amy, Beth), the variables would be Amy_A, Amy_B, Beth_A, Beth_B

- Use an int variable, where each employee is mapped to a number. For 2 shifts (A, B) and 3 employees (Amy, Beth, Carl), the variables would be A, B (which will have value 0 for Amy, 1 for Beth, 2 for Carl).

Using an int variable is usually better, since it automatically encodes the "each shift must have exactly one employee constraint" which would otherwise need to be added. That being said, sometimes the boolean model is used so a SAT solver can be used instead of a Integer Linear Programming Solver.

Typically, for theorem based solvers (such as Z3 or OR Tools), you add a group of similar constraints in a loop where you iterate through relevant variables. For instance, to add constraints for overlapping shifts, you would have a directory mapping each shift to the shifts its overlaps, and add a not equals constraint for each pair (since if they are equal, they have the same employee, and employees usually are unable to be at two places at the same time).

  for shift in shift_vars:
      for overlapping_shift in overlapping_shifts[shift]:
          solver.add(shift != overlapping_shift)

There are also local search solvers, such as Timefold, which allows you use your domain objects and functions directly in your constraints. For instance, the above constraint would look like this:

  @planning_entity
  @dataclass
  class Shift:
      employee: Annotated[Employee, PlanningVariable]
      start: datetime
      end: datetime
      
      def overlaps(self, other: 'Shift') -> bool:
          return self.start < other.end and other.start < self.end
  
  def no_overlapping_shifts(constraint_factory: ConstraintFactory):
      return (constraint_factory.for_each(Shift)
                                .join(Shift,
                                      Joiners.equal(lambda shift: shift.employee))
                                .filter(lambda a, b: a.overlaps(b))
                                .penalize(HardSoftScore.ONE_HARD)
                                .as_constraint('Overlapping Shift'))

Disclosure: I work for Timefold

[porcoda]

Read up on smt-lib: learning how to encode problems in that is a good way to start. The Python z3 bindings are a good starting point to play with it too.

[Klaus23]

https://smt.st/SAT_SMT_by_example.pdf

[3eb7988a1663]

I wish I had something to offer, but I think there is little available but grit. The solvers are magical in what they can do, but structuring a problem into the DSL is an exercise in pain. Seemingly few available public examples of patterns you can crib.