Modern SAT solvers: fast, neat and underused
codingnest.com
Modern SAT solvers: fast, neat and underused
1–10 of 46 posts
Re: Modern SAT solvers: fast, neat and underused
#2SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example.
Does anyone have good suggestions for what to use SAT solvers for?
Re: Modern SAT solvers: fast, neat and underused
#3SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
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.
Re: Modern SAT solvers: fast, neat and underused
#4SAT solvers Wikipedia: https://en.m.wikipedia.org/wiki/Boolean_satisfiability_probl...
Re: Modern SAT solvers: fast, neat and underused
#5SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
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.
Re: Modern SAT solvers: fast, neat and underused
#6Previously posted 4 months ago and 1 year ago: https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
Re: Modern SAT solvers: fast, neat and underused
#7SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
SMT solvers (which are a generalization of SAT solvers) are quite useful for program verification and symbolic execution.
Re: Modern SAT solvers: fast, neat and underused
#8SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
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.
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.
Re: Modern SAT solvers: fast, neat and underused
#9Earlier quoted context omitted.
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 favoure…
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.
Re: Modern SAT solvers: fast, neat and underused
#10Earlier quoted context omitted.
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 favoure…
> 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.