« Några fler MiniZinc-modeller, t.ex. Smullyans Knights and Knaves-problem | Main | Nya MiniZinc-modeller, flera global constraints, däribland clique »

juni 02, 2008

MiniZinc/FlatZinc version 0.8 släppt

Häromdagen släpptes en ny version av MiniZinc (se även My MiniZinc page), det constraint programming-system som jag håller på med just nu.

Den nya versionen finns här.

Förändringar
I NEWS beskrivs alla de förändringar som gjorts sedan version 0.71.

Notera att detta endast gäller MiniZinc/FlatZinc. Ändringarna är ännu (2008-06-02) inte införda för de andra solvers, dvs Gecode fz respektive ECLiPSe's ic, fd eller eplex. Jag väntar med spänning på detta.


De praktiskt viktigaste ändringarna är:

* ny deklaration av vektorer
vektorer (arrays) i högre dimensioner konverteras inte längre automatiskt till en "multi-array". Man måste deklarera dimensionen explicit.

Exempel: För att deklarera en 2-dimensionell vektor (dvs en matris) gjorde man tidigare så här:

int: n;
array[1..n, 1..n] of int: x;
% en massa andra saker
% ...
n = 3;
% deklarationen (gamla sättet)
x =
[1,2,3,
4,5,6,
7,8,9];
% ....

Nu måste man istället skriva deklarationen så här:

% ...
x =
[|1,2,3,
|4,5,6,
|7,8,9|]

Dvs man måste omsluta varje rad med ett "|"-tecken. Notera att "parenteserna" inte får delas upp utan man måste skriva "[|" respektive "|]". Gör man inte så blir det ett kryptiskt fel.


* FlatZinc har flera solvers
För FlatZinc (den solver som kommer med MiniZinc-distributionen) är default solver fd, en finite domain-solver och det var den endast som fanns tillgänglig i version 0.7.1.

Följande solvers finns nu att tillgå i FlatZinc. Från kommandot flatzinc --help:

Solver Selection Options:
-s , --solver , --solver-backend
Select the solver(s) and evaluation algorithm that should be used.
Valid solver backends are: `fd', `sat', `mip', `fdmip', `colgen',
`skp' and `ttt'. (The default is `fd'.)

--mip-solver
Use the specified solver as the default MIP solver.
Supported MIP solvers are: osi-cbc.

--sat-solver
Use the specified solver as the default SAT solver.
Supported SAT solvers are: minisat.

--colgen-mip-solver
Use the specified solver as the default MIP solver for the column
generation backend. (Note that this choice will be overridden by
a `colgen_master_solver' annotation in the model.)
Supported column generation MIP solvers are: osi-cbc.

--colgen-approx-solver
Use the specified approximate linear solver with the column
generation backend. (Note that this choice will be overridden by
a different choice inside a `colgen_master_solver' annotation in
the model.)
Supported approximate linear solvers are: osi-volume.

Speciellt intressanta är fd, mip (mixed integer programming, använder Coin:s osi-cbc) och fdmip (en hybrid mellan dessa).

Det antyds att allt utom fd och möjligen mip/fdmip bör anses som odokumenterade features.

Tyvärr generar flatzinc-programmet endast en lösning. Hoppas att man ändrar detta i en senare version så att alla lösningar visas (som Gecode fz och ECLiPSe's ic/fd gör).


* show_cond
När man skriver ut resultaten, med show(variabel) inom output, har man endast kunnat för if-satser på fixa variabler (dvs par-deklarerade variabler), vilket har begränsat uttryckfullheten ordentligt.

I version 0.8 finns det möjlighet att med show_cond göra en dynamisk kontroll av icke-fixa variabler. Exempel: Här skriver vi endast ut de värden som tillsammans blir 14, dvs de som har värdet 1 i x-vektorn. MiniZinc/FlatZinc skriver ut 2 3 4 5.

int: n = 10;
array[1..n] of var 0..1: x;

solve satisfy;
constraint sum(i in 1..n) (x[i]*i) = 14;

output [
show_cond(x[i] > 0, i, "") ++ " "
| i in 1..n
];


* vektorer är 1-baserade
I äldre versionen var alla vektorer 0-baserade (dvs första element räknades från 0). Nu börjar man på 1 istället. Normalt behöver man inte bry sig om, detta förutom då man arbetar med "slices" som skickas till ett predikat.


Mina exempel
Mina MiniZinc-modeller på My MiniZinc page är fortfarande i gamla 0.7.1-formatet, och jag kommer att vänta med att konvertera dem till version 0.8 tills åtminstone en av de två andra solvers (Gecode fz respektive ECLiPSe's varianter) stöder denna version. Då är det förmodligen endast vektor-deklarationerna som kommer att ändras (men kanske en och annan show_cond läggs till).


Wrapper
För övrigt har jag skapat en flexibel Perl-wrapper kring de olika solvers. Det har stöd för både 0.7.1 och den nya 0.8. Och man kan från kommandoraden t.ex. ändra parametrar, lägga till constraints, ändra antal lösningar som ska visas etc.

Jag har ännu inte några planer att lägga upp detta program publikt, men maila mig gärna om du är intresserad av det. Som en teaser visas två exempel som faktiskt inte är helt ovanliga:

mzx.pl model.mzn --solver minizinc --new --option "--solver fdmip" --param "n=10;k=3"

mzx.pl model.mzn --solver ic --param "n=100;k=12" --num_solutions 10

Det första exemplet kör den nya versionen av MiniZinc (oftast SVN-versionen) med solvern fdmip, och ändrar parametern n till 10 samt parametern k till 3. Det andra exemplet kör ECLiPSe's ic-solver med andra parametrar samt visar endast de 10 första lösningarna.


Posted by hakank at juni 2, 2008 06:10 EM Posted to Constraint Programming