MiniZinc: free and open-source constraint modeling language
minizinc.org
minizinc.org
One thing I'm interested to know (as someone with less experience in constraint programming), is when does one employ constraint programming engines like Choco, Gecode, MiniZinc etc, vs. when metaheuristics (such as simulated annealing, genetic algorithms, etc.) are a more practical solution. Is there a rule of thumb regarding the size search space, type of problem etc. ?
Local search is always going to outperform global search but there’s no guarantee of a solution or an optimal one. So it really depends on your needs and how long you’re prepared to wait. Modern CSP solvers can handle impressively large problems with multiple thousands of clauses (1m+ for SAT), but it really depends on what your constraints look like.
You need to know the actual optimal answer (metaheurisitics can never prove they have the optimal).
You need all solutions to your problem.
Your problem is just true/false, not optimisation, and there is no obvious way to measure the quality of a partial solution (so metaheurisitics will struggle).
In general, CP does better on smaller, harder problems.
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.
Different heuristics work best for different workloads, so you get solvers that are specialized for a single domain.
Modern SAT solvers use the DPLL algorithm, which has in turn influenced modern CSP solvers. Wikipedia has a great page on DPLL:
x = z3.BitVec('x', 32)
y = z3.BitVec('y', 32)
i1 = x | y
i2 = ~(~x | ~y)
s = z3.Solver()
s.add(i1 != i2)
if s.check() == z3.sat:
print "found counterexample"
print s.model()
else:
print "always equal"Some solvers, e.g. Gecode and JaCoP, can handle nonlinear problems with floats as well as finite-domain problems.
(I used constrained quadratic optimization to fit transition matrices to population data for my dissertation, and for some other demographic estimation projects.)