Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

MiniZinc: free and open-source constraint modeling language

minizinc.org

Post reply on HN
Print view View original

21–30 of 34 posts

Re: MiniZinc: free and open-source constraint modeling language

#21

Post by sevensor »

jsjolen wrote: post #20

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…

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.

Re: MiniZinc: free and open-source constraint modeling language

#22

Post by placebo »

Macuyiko wrote: post #5

Every time some OR or constraint programming language comes up, Håkan Kjellerstrand is an obligatory mention. He has a whole page dedicated to problems and examples for those, including MiniZinc: http://www.hakank.org/minizinc/index.html

Yes, an impressive set of problems solved with an impressive set of solvers. Quite a bit of experience stored on that site.

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. ?

Re: MiniZinc: free and open-source constraint modeling language

#23

Post by jahewson »

placebo wrote: post #22
Macuyiko wrote: post #5

Every time some OR or constraint programming language comes up, Håkan Kjellerstrand is an obligatory mention. He has a whole page dedicated to problems and examples for those, including MiniZinc: http://www.hakank.org/minizinc/index.html

Yes, an impressive set of problems solved with an impressive set of solvers. Quite a bit of experience stored on that site. 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…

Constraint satisfaction is NP-complete and for optimization it’s NP-hard. In theory that means it’s going to be equally hard to determine how many steps solving the problem takes as it is to simply solve the problem.

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.

Re: MiniZinc: free and open-source constraint modeling language

#24

Post by yorwba »

sevensor wrote: post #21
jsjolen wrote: post #20

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…

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.

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.

Re: MiniZinc: free and open-source constraint modeling language

#25

Post by jahewson »

sevensor wrote: post #21
jsjolen wrote: post #20

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…

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.

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

Re: MiniZinc: free and open-source constraint modeling language

#26

Post by jahewson »

crimsonalucard wrote: post #2

What is a constraint modeling language exactly? I briefly looked at the first example in the documentation, and it looks like you specify a problem and some type of solver solves the problem automatically? What algorithm is it running exactly?

“Constraint Programming” refers, for the most part, to the solving of finite-domain problems via backtracking and constraint propagation and is typically concerned with performing a complete, global search of the solution space.

https://en.m.wikipedia.org/wiki/Constraint_satisfaction

Re: MiniZinc: free and open-source constraint modeling language

#28

Post by crimsonalucard »

jahewson wrote: post #26
crimsonalucard wrote: post #2

What is a constraint modeling language exactly? I briefly looked at the first example in the documentation, and it looks like you specify a problem and some type of solver solves the problem automatically? What algorithm is it running exactly?

“Constraint Programming” refers, for the most part, to the solving of finite-domain problems via backtracking and constraint propagation and is typically concerned with performing a complete, global search of the solution space. https://en.m.wikipedia.org/wiki/Constraint_satisfaction

I like this answer. However, by solution space do you mean domain space?

Re: MiniZinc: free and open-source constraint modeling language

#30

Post by CJefferson »

placebo wrote: post #22
Macuyiko wrote: post #5

Every time some OR or constraint programming language comes up, Håkan Kjellerstrand is an obligatory mention. He has a whole page dedicated to problems and examples for those, including MiniZinc: http://www.hakank.org/minizinc/index.html

Yes, an impressive set of problems solved with an impressive set of solvers. Quite a bit of experience stored on that site. 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…

One easy rule is use CP when One of these are true.

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.

Post reply on HN