3 ms·

So 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, tryin

So 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 ago
The 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 ago
Z3 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 ago
I 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 ago
  So 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?

yorwba 9y ago

The 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 ago

Z3 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 ago

I 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 ago
So 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?