Tried to use MiniZinc to write a model checker [1] for c programs a while back [2]. Essentially checking the equivalence of c functions that use only bit operations. It basically translates the programs into minizinc, then attempts to derive a case where the same input results in differing output. Was a fun way to experiment using the constraint solver for a practical application, though unfortunately didn't work as well on larger more complicated functions.
MiniZinc: free and open-source constraint modeling language
11–20 of 34 posts
Re: MiniZinc: free and open-source constraint modeling language
#12Fun fact: We're using MiniZinc and Gecode in production code to solve volume/product puzzles on oil tankers.
Re: MiniZinc: free and open-source constraint modeling language
#13What 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?
Possibly a simplex solve for a large linear problem.
There is a lot off different type of solvers that can be used to solve a MiniZinc model: MIP, Constraint Programming, SAT, Hybrid SAT+CP, Local search etc.
Re: MiniZinc: free and open-source constraint modeling language
#14Tried to use MiniZinc to write a model checker [1] for c programs a while back [2]. Essentially checking the equivalence of c functions that use only bit operations. It basically translates the programs into minizinc, then attempts to derive a case where the same input results in differing output. Was a fun way to experiment using the constraint solver for a practical application, though unfortunately didn't work as…
I'd expect a SMT (Satisfiability modulo theory) solver like z3 to work better for this use case, might be worth giving it a try. E.g.
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"Re: MiniZinc: free and open-source constraint modeling language
#15What 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?
MiniZinc is a modeling language - for problem specification. Then there are solvers that understand MiniZinc (Gecode, ECLiPSe, Google OR-Tools, ...), and they use variety of algorithms (mixed linear programming, constraint-specific algorithms, local search, SAT-solving techniques, ...). You can use the same specification of the problem in MiniZinc with different solvers.
Re: MiniZinc: free and open-source constraint modeling language
#16People need to specify what type of constraint their solver handles. It's a rather large space, and to not even mention what type of constraints on the page is a major oversight.
Hear, hear. Is this good for optimization problems over the reals, or only finite-domain problems? If the former, can it solve nonlinear problems?
It depends on the solver backend. Some only solve finite domain problems. I think all of them (for general constraint programming) can solve non-linear problems. Obviously if you use a backend that only solves mixed integer linear programs, then you are more restricted.
Re: MiniZinc: free and open-source constraint modeling language
#17People need to specify what type of constraint their solver handles. It's a rather large space, and to not even mention what type of constraints on the page is a major oversight.
Hear, hear. Is this good for optimization problems over the reals, or only finite-domain problems? If the former, can it solve nonlinear problems?
Some of the FlatZinc solvers can handle (nonlinear) finite-domain problems, and some just linear MIP problems with floats.
Some solvers, e.g. Gecode and JaCoP, can handle nonlinear problems with floats as well as finite-domain problems.
Re: MiniZinc: free and open-source constraint modeling language
#18Earlier quoted context omitted.
Hear, hear. Is this good for optimization problems over the reals, or only finite-domain problems? If the former, can it solve nonlinear problems?
Some of the FlatZinc solvers can handle (nonlinear) finite-domain problems, and some just linear MIP problems with floats. Some solvers, e.g. Gecode and JaCoP, can handle nonlinear problems with floats as well as finite-domain problems.
the hakank?
Re: MiniZinc: free and open-source constraint modeling language
#19Earlier quoted context omitted.
Some of the FlatZinc solvers can handle (nonlinear) finite-domain problems, and some just linear MIP problems with floats. Some solvers, e.g. Gecode and JaCoP, can handle nonlinear problems with floats as well as finite-domain problems.
the hakank?
:-) Yes.
Re: MiniZinc: free and open-source constraint modeling language
#20A 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.