4 ms·

At a local group we have weekly meetings where we cook dinner. Two people cook, and two people do the dishes. I used a SAT solver (z3) to find optimal schedule

At a local group we have weekly meetings where we cook dinner. Two people cook, and two people do the dishes. I used a SAT solver (z3) to find optimal schedules given that people want the tasks to be distributed fairly, but also given other secondary criteria such as mixing up which pairs cook together, prevent being assigned a task two weeks in a row or getting the same task twice in a row, etc.

nurettin 7y ago
It is pretty easy to come up with an integer space in order to simulate week days, the concept of consecutiveness and homogeneous distribution. However, as soon as we get custom rules and exceptions things start to become impossible and we have to start inventing a best effort solution which turns into minimization or maximization of each human variable. At this point some humans with higher status want to be favoured and you get a tug of war instead of an sat solver problem where nothing you suggest pleases anyone because they have a life and can't afford to tell you every little detail that interests them and they go back to manually picking their dates.
- roenxi 7y ago
  In corporate deployment of a SAT or even a linear solver one of the bigger challenges is convincing people to solve the SAT/linear problem and then stop. I'd guess that most corporate deployments of a solver are (1) solve the easy part (2) add one extension to try and deal with a difficult part (3) deployment finishes because cost of a 2nd extension is too high, either computationally or in development time. I think there is a big untapped corporate demand for evolutionary optimisers. They scale a bit closer to problem difficulty as measured by humans and people get dazzled by the idea of finding an optimal solution to a bad model rather than an OK solution to an OK model of reality which is more flexible.
- wenc 7y ago
  > they go back to manually picking their dates. I'm not sure if it's all or nothing. SAT are concerned with satisfying constraints, so you get feasible solutions. A feasible solution merely satisfies constraints, and does not take objectives into account. The optimization-equivalent is an Integer Program (IP), which gives you optimal solutions for a given objective function while satisfying all constraints. Most complex scheduling problems are solved as IPs or MIPS (Mixed Integer Programs). Priorities can be modeled as weights. Even if everybody's preferences cannot be met, you can arrive at some sort of weighted compromise (either in a least-squares sense, or some user-defined distance metric) The best MIP solvers today (e.g. CPLEX, Gurobi, Xpress) solve problems with 100k variables without breaking a sweat (caveat: they do not handle nonconvexities, but good modelers know how to develop linear/convex formulations). They are used in applications ranging from hospital scheduling to airline scheduling to oil refinery scheduling. In my experience computer scientists typically know about SAT solvers but only a small subset know about MIP solvers. Knowing about the latter expands one's horizons on what's possible.
  - nurettin 7y ago
    What I meant was, human capriciousness is hard to model and they change their initial premises on a whim. Especially in academic environments. On the other hand, military and hospital applications won't show that weakness.
    - wenc 7y ago
      Human capriciousness is indeed hard to model, so one solution is not do it. In timetabling applications, the algorithm provides a level of impartiality so even if some constituents don't get what they want, you can always blame the algorithm -- "it tried, but it had to satisfy other constraints". This removes some (but not all) of the politics behind timetabling. Influential persons may still try to wield their political power to bend the algorithm toward favoring them (e.g. in algorithmic terms, this could mean boosting their weight from 0.5 to 0.8 to beat out competition) but even in this compromised state, optimal timetabling is still better than doing it manually -- the optimization algorithm will at least try to maximize remaining preferences within the remainder degrees-of-freedom. Timetabling is an inherently political process anywhere (if one has ever done timetable for high school teachers....), but optimization algorithms do bring a level of impartiality to the process. Also, if folks aren't explicit about their preferences, or change their minds, it's no fault of the algorithm.
  - salty_biscuits 7y ago
    ... only a small subset know about MIP solvers And an even smaller subset are willing to pay to use gurobi or cplex. It would be so nice if the open source alternatives had competitive performance!
    - nurettin 7y ago
      In your experience, does google's or-tools library have any chance in comparison?
      - disjhshava 7y ago
        I didn't benchmark it and can't give a speed comparison, but I had success solving a pretty big optimization problem with GLOP, which I beleive uses or-tools.
mabbo 7y ago
That's fascinating! I've always wanted to build a similar system for assigning chores around the house based on everyone "bidding" on how much they see the effort of each chore being. In theory, one should be able to come up with an assignment where everyone believes they're doing less than everyone else, by their own metric of work effort. Applying computer science to everyday life is so rare but lovely.
- Pamar 7y ago
  I studied Simplex and related techniques at University, and took https://courses.edx.org/courses/course-v1:MITx+15.053x+3T2016/course/ https://courses.edx.org/courses/course-v1:MITx+15.053x+3T201... as a refresher. The course is now closed, but you can probably find something similar as a MOOC.

nurettin 7y ago

It is pretty easy to come up with an integer space in order to simulate week days, the concept of consecutiveness and homogeneous distribution. However, as soon as we get custom rules and exceptions things start to become impossible and we have to start inventing a best effort solution which turns into minimization or maximization of each human variable. At this point some humans with higher status want to be favoured and you get a tug of war instead of an sat solver problem where nothing you suggest pleases anyone because they have a life and can't afford to tell you every little detail that interests them and they go back to manually picking their dates.

roenxi 7y ago
In corporate deployment of a SAT or even a linear solver one of the bigger challenges is convincing people to solve the SAT/linear problem and then stop. I'd guess that most corporate deployments of a solver are (1) solve the easy part (2) add one extension to try and deal with a difficult part (3) deployment finishes because cost of a 2nd extension is too high, either computationally or in development time. I think there is a big untapped corporate demand for evolutionary optimisers. They scale a bit closer to problem difficulty as measured by humans and people get dazzled by the idea of finding an optimal solution to a bad model rather than an OK solution to an OK model of reality which is more flexible.
wenc 7y ago
> they go back to manually picking their dates. I'm not sure if it's all or nothing. SAT are concerned with satisfying constraints, so you get feasible solutions. A feasible solution merely satisfies constraints, and does not take objectives into account. The optimization-equivalent is an Integer Program (IP), which gives you optimal solutions for a given objective function while satisfying all constraints. Most complex scheduling problems are solved as IPs or MIPS (Mixed Integer Programs). Priorities can be modeled as weights. Even if everybody's preferences cannot be met, you can arrive at some sort of weighted compromise (either in a least-squares sense, or some user-defined distance metric) The best MIP solvers today (e.g. CPLEX, Gurobi, Xpress) solve problems with 100k variables without breaking a sweat (caveat: they do not handle nonconvexities, but good modelers know how to develop linear/convex formulations). They are used in applications ranging from hospital scheduling to airline scheduling to oil refinery scheduling. In my experience computer scientists typically know about SAT solvers but only a small subset know about MIP solvers. Knowing about the latter expands one's horizons on what's possible.
- nurettin 7y ago
  What I meant was, human capriciousness is hard to model and they change their initial premises on a whim. Especially in academic environments. On the other hand, military and hospital applications won't show that weakness.
  - wenc 7y ago
    Human capriciousness is indeed hard to model, so one solution is not do it. In timetabling applications, the algorithm provides a level of impartiality so even if some constituents don't get what they want, you can always blame the algorithm -- "it tried, but it had to satisfy other constraints". This removes some (but not all) of the politics behind timetabling. Influential persons may still try to wield their political power to bend the algorithm toward favoring them (e.g. in algorithmic terms, this could mean boosting their weight from 0.5 to 0.8 to beat out competition) but even in this compromised state, optimal timetabling is still better than doing it manually -- the optimization algorithm will at least try to maximize remaining preferences within the remainder degrees-of-freedom. Timetabling is an inherently political process anywhere (if one has ever done timetable for high school teachers....), but optimization algorithms do bring a level of impartiality to the process. Also, if folks aren't explicit about their preferences, or change their minds, it's no fault of the algorithm.
- salty_biscuits 7y ago
  ... only a small subset know about MIP solvers And an even smaller subset are willing to pay to use gurobi or cplex. It would be so nice if the open source alternatives had competitive performance!
  - nurettin 7y ago
    In your experience, does google's or-tools library have any chance in comparison?
    - disjhshava 7y ago
      I didn't benchmark it and can't give a speed comparison, but I had success solving a pretty big optimization problem with GLOP, which I beleive uses or-tools.

mabbo 7y ago

That's fascinating! I've always wanted to build a similar system for assigning chores around the house based on everyone "bidding" on how much they see the effort of each chore being. In theory, one should be able to come up with an assignment where everyone believes they're doing less than everyone else, by their own metric of work effort. Applying computer science to everyday life is so rare but lovely.

Pamar 7y ago
I studied Simplex and related techniques at University, and took https://courses.edx.org/courses/course-v1:MITx+15.053x+3T2016/course/ https://courses.edx.org/courses/course-v1:MITx+15.053x+3T201... as a refresher. The course is now closed, but you can probably find something similar as a MOOC.