41–46 of 46 posts
SAT 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?
Earlier quoted context omitted.
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 t…
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?
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)Earlier quoted context omitted.
> 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 comp…
... 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!
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.
Earlier quoted context omitted.
... 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!
In your experience, does google's or-tools library have any chance in comparison?
SAT 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?