I have used the Z3 solver(https://github.com/Z3Prover/z3) to optimize a job scheduling problem. Roughly, I have ~20k jobs, defined by N tasks (~1-50). A job is complete only if M tasks (typically 2-3) per job are done. Every task takes some variable amount of time to complete and can only be run during specific windows. Given the equipment can only perform P tasks in parallel, what is the optimal configuration of tasks (~500k) that will allow us to complete the most jobs?

The search space for this problem is enormous, but Z3 will produce an impressive result within a few minutes.

amazing, I tried doing this recently but I guess my modeling was not good enough and it would take hours to find the solution with a couple of dozen variables. Do you have any pointers on how to much these types of problems with a SMT/SAT solver efficiently?

The documentation and API quirks of z3 also led me down some performance sinks before I was able to tackle the larger models. Not a Z3/SMT expert, but what worked for me was to model every time tick as the sum of all tasks that could be performed at that instant. Set a constraint on each tick that sets the sum of these tasks to be <= P. Add the book-keeping on the task-job relationships and that was it.

Using the Python bindings, the biggest performance impact I discovered was ensuring that my jobs and tasks were represented as z3.Bool and not z3.Int (requiring a roundabout way to do a summation on z3.Bools). Something like:

  tasks_this_tick = [(z3.Bool(task_id), 1) for task_id in current_tasks]
  model.add(z3.PbLe(tasks_this_tick, max_tasks_per_tick + 1)

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.

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.

> 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.

... 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!

Depends on the problem

Cbc [1] is modern, free and is competitive for most non-complex problems like timetabling (say less than 100k variables). (Cbc is much better than GNU Linear Programming Kit -- GLPK -- which uses outdated algorithms and is not competitive). Cbc can also be called from Excel via OpenSolver.

Scip [2] is the most performant "non-commercial" solver, but is only free for non-commercial uses. Commercial uses require licensing.

As for writing MIPs, this FICO MIP formulation guide [3] is extremely well written. Modeling MIPs is something of an art, and this doc captures most of the common formulations.

[1] https://github.com/coin-or/Cbc

[2] https://scip.zib.de/

[3] https://www.fico.com/en/resource-download-file/3217

In your experience, does google's or-tools library have any chance in comparison?

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.

The entire US power grid commits generators and dispatches them using MIP solvers. This is a pretty enormous problem with hard time constraints. We're talking about millions of constraints.

Edit: well to be more specific, commitment is done with MIP solvers (difficult problem) and dispatch is done with LP solvers (easy and fast).

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.

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.

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.

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.

I studied Simplex and related techniques at University, and took 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.

SMT solvers (which are a generalization of SAT solvers) are quite useful for program verification and symbolic execution.

These can be deployed against the Eternity II puzzle. I doubt any SAT solver will find a complete solution in our lifetimes, but a near solution would be satisfying.

https://en.wikipedia.org/wiki/Eternity_II_puzzle

> satisfying

Heh.

I have applied SATs with some success to generative models where sampling methods would not work well, e.g. if you have many soft and hard constraints. Another alternative is to use neural guides.

do you have any pointers on modeling with soft/hard constraints and SAT solvers?

I've done some program synthesis and equivalence proving with them. It was for sure trivial to express and nontrivial to express in a way that would actually get to a solution. I know of no general shortcuts for avoiding the part where it performs terribly for nonobvious reasons, but then I am not a SAT solver expert.

I've also done a bit of work on concolic execution, which has yielded interesting insights but not useful results. I'll probably write something up for hn if/when it does yield results.

As others have said, my first real use of it was for scheduling problems. It works but isn't really better than a hand rolled naive solver for the scale of problem I was looking at.

They seem to be good for proving obvious things about cryptosystems. It's very interesting to see how quickly block length becomes a security parameter for things like Speck.

Overall I like them and they clearly have potent uses, but... often I find myself shrugging, accepting some constraint, and using the more obvious approach. It may be that I just seldom have to solve a hard enough problem with full generality.

I'm the same with Prolog. I love the language, but I have only once worked somewhere that used it for an actual problem.

I used one to do the seating arrangement at my wedding. Doing it well manually is nearly impossible if you have a lot of constraints.

libsolv, a free package dependency solver using a satisfiability algorithm.

https://github.com/openSUSE/libsolv

https://en.opensuse.org/openSUSE:Libzypp_satsolver

The meteor framework uses it for dependency resolution in their package system.