5 ms·
A constraint solver typically works by: 1. Having a finite set of variables with a finite set of possible values 2. Having a finite set of propagators which a
by jsjolen 9y ago
A constraint solver typically works by:
1. Having a finite set of variables with a finite set of possible values
2. Having a finite set of propagators which are monotonic on variables (that is, it either reduces the amount of possible values for a variable or does not (it never adds).
3. A space describing a full set of variables and propagators
4. A way of reducing the amount of values when all propagators have hit a fixpoint for some space.
5. A way of rewinding state when some variable runs out of possible values
And then it basically (BASICALLY) runs this loop:
while(!solved(space)) {
if(failed(space)) {
rewind(space);
}
while(!fixpoint(space)) {
for(p in propagators(space))
{ p(space);
}
}
make_choice(space);
}
It's mainly used for solving NP-hard problems by being smart when attacking the full search tree.
- sevensor 9y agoSo what differentiates the solvers then? Is it in how they apply the propagators? I'm interested because I naively wrote the exact loop you just posted, trying to solve a very hard problem. I spent ages trying different heuristics, but I knew I was floundering. Then I discovered Z3, which solves the problem in a tiny fraction of the time. It seems like pure magic, and I'm keen to understand how it works.
- yorwba 9y agoThe two points where clever heuristics can be applied are in make_choice (i.e., which variable to set such that the search space is maximally reduced) and in rewind (i.e., which variable to unset to make the problem hopefully satisfiable again). Different heuristics work best for different workloads, so you get solvers that are specialized for a single domain.
- jahewson 9y agoZ3 is an SMT solver, which means it combines a boolean SAT solver, which is used to solve the boolean structure of the problem, with theory-specific solvers, e.g. bit vectors, or linear equations. Modern SAT solvers use the DPLL algorithm, which has in turn influenced modern CSP solvers. Wikipedia has a great page on DPLL: https://en.m.wikipedia.org/wiki/DPLL_algorithm https://en.m.wikipedia.org/wiki/DPLL_algorithm
- afpx 9y agoI haven’t used all the different solver engines, and I haven’t kept up with the field, but many years ago I had a license to IBM ILOG CPLEX, and it was interesting how much faster it was than some others. Gurobi is also very fast (I think they were started by the people who sold ILOG CPLEX to IBM), but haven’t benchmarked it vs CPLEX.
- sevensor 9y agoSo I haven't looked deeply into the capabilities of Gurobi and CPLEX, but I was under the impression that they focus on integer linear programming. How do they do with problems for which finding a feasible solution is very difficult?