hakank.blogg: Constraint Logic Programming Archives

april 14, 2008

MiniZinc-sida samt fler MiniZinc-exempel

För en vecka sedan skrevs Constraint Programming: Minizinc, Gecode/flatzinc och ECLiPSe/minizinc, där bland annat några MiniZinc-exempel förevisades.

Sedan dess har jag renskrivit några andra av mina MiniZinc-modeller, dvs översatt kommentarer till engelska, tagit bort fåniga utrop samt givit någon form av problemreferens. Dessa finns nu på en egen MiniZinc-sida: My MiniZinc page tillsammans med andra relevanta länkar. Det finns för tillfället drygt 100 modeller (program) inom olika områden, där några listas nedan (det finns alltså fler på sidan).

Rubrikerna är (som alla indelningar) arbiträra och ofullständiga (men trots det bra att ha). Jag har inte - förutom i något enstaka fall - tagit med problem/modeller som finns på MiniZinc-exempelsidan (vilken se).

Som grädde på moset finns även en modell som uppstod i samband med läsandet av Ravens Internationell på kontoret. Nämligen (den naturligtvis Vennska) funderingen: givet fördelning av språken, hur är då fördelningen per person. Det finns en massa lösningar. Problemet undersöks i Raven puzzle.

Posted by hakank at 06:58 EM Posted to Constraint Logic Programming | Comments (0)

april 05, 2008

Constraint Programming: Minizinc, Gecode/flatzinc och ECLiPSe/minizinc

Minizinc är ett relativt nytt constraint programming-system (startade 2005). Det tillhör G12-projektet som är menat att bli ett öppet (som i open source) state-of-the-art-system.

Samtidigt som det mer kompletta systemet Zink håller på att utvecklas, utvecklas Minizinc en mindre variant som även föreslås att användas som ett gemensamt språk för benchmarks av olika constraint solvers (dvs de system som faktiskt löser problemen, se nedan).

Zinc (storebrodern) finns inte tillgängligt för närvarande. Det finns däremot Minizinc, dels i en officiell version 0.7.1, dels en utvecklingsversion (jag använder utvecklingsversionen). Se vidare Download för nedladdningar.

Specifikationen för både Zinc och MiniZinc är Zinc spec (PDF). Detta dokument och andra nyttigheter finns via MiniZinc and FlatZinc. Uppdaterade versioner av dokumenten finns i utvecklingsversionen.

Många Minizinc-exempel finns här. Fler exempel finns i distributionens kataloger examples respektive benchmark samt till viss del i katalogen test/minizinc.

Jag tycker att Minizinc är ett mycket trevligt och lättarbetat system. Språket har syntaktiskt socker på en bra nivå och är numera min favorit bland constraint programming-systemen.

Det kommer att bli mycket intressant när Zinc släpps eftersom det har en massa skoj finesser som jag saknar i Minizinc, men jag lämnar det för nu. Här nedan kommer jag alltså i stort sett endast att prata om Minizinc.

Lite om Minizinc

En av de stora fördelarna med att använda constraint programming-språk liknande Minizinc är att de är deklarativa, dvs man beskriver vad som ska göras och inte hur saker ska göras (så är i alla fall idealet).

Prolog är ett av de mest kända exemplen på denna typ av programspråk. [Några mindre kända sådana språk är inom stable models/answer set programming-paradigmet såsom smodels/lparse, som nog kan uppfattas som än mer magiska än Prolog.]

Minizinc är dock inget "komplett programspråk" såsom Prolog, t.ex. saknas stöd för rekursion (detta av design för att göra det enkelt att arbeta med för olika solvers), det finns ingen filläsning förutom inkluderande av andra Minizinc-modeller eller data, hantering av strängar är synnerligen begränsat etc.

Trots dessa begränsningar är kan väldigt många problem modelleras i Minizinc. Se den officiella exempelsamlingen som innehåller olika typer av standardproblem från constraint programming, operations research och matematisk programmering. Nedan finns något av det som jag själv knåpat ihop.

Några speciellt trevliga saker i Minizinc

- definition av predicate

Man kan definiera predikat som sedan kan återanvändas via include-direktivet. Det finns en samling sådana i lib/zinc/globals.mzn som är väl värt att studera.

(I Zinc kommer det att finnas möjlighet att definiera funktioner som returnerar värden, men i Minizinc använder man samma teknik som i Prolog för att "returnera" värden, dvs att ange returvärdet i parameterlistan.)

- "bidirectional" predikat

Liksom Prolog har Minizinc den trevliga egenskapen att predikat kan vara "bidirect", dvs att flödet mellan parametrarna kan verka åt båda hållen, kan vara ut- eller in-data. Ett enkelt exempel på detta är konvertering mellan tal och en vektor (givet en bas). Jag har definierat toNum på följande sätt.
predicate toNum(array[int] of var int: vec, var int: n, float: base) = let { int: len = length(vec) } in % summera ihop elementen i vec för den givna basen n = sum(i in 1..len) ( ceil(pow(base, int2float(len-i))) * vec[i] % se nedan för varför denna används ) % samtliga element i vec måste vara 0 /\ forall(i in 1..len) (vec[i] >= 0) ;

Poängen är att man kan använda detta predikat för att konvertera från ett decimaltal (n) till en vektor (vec) av heltal i den givna basen base, eller konvertera från vektorn av heltal till ett tal (givet en bas). toNum används t.ex. i debruijn_binary.mzn, vilken se. (I teorin skulle man också kunna räkna ut vilken bas som används givet vec och n, men det går inte i Minizinc eftersom pow() inte kan användas på en var-deklarerad variablen utan måste definieras som en fix parameter.)

Här blir n = 7
% ... constraint % .... toNum([1,1,1], n, 2.0) ;

och här blir vec = [1,1,1]:
% ... constraint % ... toNum(vec, 7, 2.0) ;

Det är mycket denna bidirektionella egenskap gör att programmering i Minizinc (och liknande deklarativa språk) känns riktigt magiskt. Och det är synnerligen skoj.

Tyvärr är Minizinc hårt typat så man måste själv konvertera flyttal till heltal, vilket frustrerar mig. [I Zinc/Minizinc-specen står att sådan konvertering kommer att göras automatiskt i storebroderna Zinc, men inte i Minizinc. Jag hoppas att specifikatörerna besinnar sig.] Och eftersom pow()-funktionen för heltal inte funkar i den aktuella versionen är man tvungen att använda float-varianten vilket innebär att man måste använda göra ceil(...)-hacket. Det är ju en hel del sådant i betaversioner som det tar tid att komma på och runt.

Ett något mer avancerad exempel på bidirection är mortgage.mzn (beräkning av lån), som är ett (annat) standardexempel i constraint logic programming (där ofta just Prolog användas som grund eller inspiration för implementationerna). På samma sätt som i toNum kan samma kodbas - med olika initialvärden - användas för att räkna ut de andra parametrarna. Se kommentarerna i programmet för vidare info. Not: för närvarande är det endast ECLiPSe-solvern som klarar detta problem.

Exempel på mer användande av toNum finns i programmen debruijn_binary och gray_code.mzn som beskrivs mer nedan.

* global constraints

I filen lib/zinc/globals.mzn finns ett flertal "global constraints" implementerade (och det antyds att det kommer att fyllas på med fler). Global constraints kan ses som standardrutiner ("standardmönster") att lösa vissa typer av (del)problem, t.ex. all_different(x) som kräver att samtliga element i en vektor ska vara olika, global_cardinality_constraint som räknar hur antal förekomster av olika element det finns i en vektor (och med bidirect-principen kan man ställa krav på antalet förekomster), etc.

Det finns en stor samling definitioner/beskrivningar av sådana global constraints (men tyvärr inga implementationer) i Global Constraint Catalog.

Min personliga fascination för sådana globala constraints är på modelleringsnivå eftersom de kan ses som byggstenar (tankehjälp) för modellering. Som övning har några av dessa implementerats såsom circuit.mzn (som i min implementation bygger på några observationer kring s.k. orbits i permutationer), cycle etc.

En stora vinst med sådana global constraints är att underliggande solvers kan göra specialoptimimeringar, vilket naturligtvis snabbar upp systemen. Studiet av sådana global constraints är en viktig del i forskningen kring constraint programming.

* stöd för flera olika solvers

Språket Minizinc är egentligen bara en del av systemet och det löser inga problem. I stället konverteras till ett annat språk (Flatzinc) som olika solvers kan arbeta med för att faktiskt lösa problemet. (Man skulle kunna översätta "solver" med "problemlösare", men eftersom det ryser varje gång jag använder den svenska versionen av Excels Solver så gör jag inte det :-). I distributionen finns det en solver med: flatzinc.

Redan nu finns det redan tre solvers: flatzinc, Gecode/flatzinc samt ECLiPSe-modulen minizinc. De gås igenom nedan.

Exempel

Som första lite längre kommenterade exempel visas här SEND + MORE = MONEY-problemet (saknas av någon anledning i Minizinc-exempelsamlingen). Problemet är helt enkelt: Byt ut bokstäverna mot unika siffror (0..9) i additionen SEND + MORE = MONEY. Det är ett paradigmatiskt exempel (dvs har "Hello, world"-status) i constraint programming-världen och finns i alla läroböcker.

Så här ser min rättframma implementation ut:
% globals.mzn innehåller den globala constrainten all_different include "globals.mzn";



% definierar varje bokstav som en variabel

% de är samtliga heltal mellan 0 och 9

var 0..9: S;

var 0..9: E;

var 0..9: N;

var 0..9: D;

var 0..9: M;

var 0..9: O;

var 0..9: R;

var 0..9: Y;

% vektorrepresentationen av de 8 variablerna för att kunna

% använda all_different

array[1..8] of var int: fd =

  [S,E,N,D,M,O,R,Y];



%

% De olika begränsningarna som ska göras, både för själva problemet och

% eventuella hjälpstrukturer

%

constraint

  % all_different kräver att alla siffror ska vara olika

  all_different(fd) /\

  

  % definiera själva problemet, dvs hur relationen mellan bokstäverna

  % ser ut

            1000*S + 100*E + 10*N + D  +  

            1000*M + 100*O + 10*R + E  = 

  10000*M + 1000*O + 100*N + 10*E + Y 

  /\

  % varken S eller M får vara 0

  S > 0 /\

  M > 0

;  

%

% solve satisfy ger en lösning, dvs inget att minimera eller maximera

% 

solve satisfy;

%

% utskriften

%

output [

   %   show(fd), "\n",

   "S:", show(S), " E:", show(E), " N:", show(N), " D:", show(D), 

   " M:", show(M), " O:", show(O), " R:", show(R), " Y:", show(Y),

   "\n\n",

   "    ", show(S), show(E), show(N), show(D),"\n",

   " +  ", show(M), show(O), show(R), show(E),"\n",

   " = ",  show(M), show(O), show(N), show(E), show(Y), "\n"

];

Sedan kör man programmet lite olika beroende på vilken solver man använder. Jag brukar testa med samtliga tre för att se vilken som är snabbast etc.

Minizinc (anropar flatzinc automatiskt)
minizinc send_more_money.mzn

eller programmet flatzinc direkt via konvertering till .fzn-format.

mzn2fzn send_more_money.mzn flatzinc send_more_money.fzn

Gecode/flatzinc:
mzn2fzn send_more_money.mzn fz send_more_money.fzn

ECLiPSe:
eclipse -e "minizinc:mzn_run('send_more_money.mzn',zn_options{solver:fzn_ic})"

Resultatet blir samma för alla
S:9 E:5 N:6 D:7 M:1 O:0 R:8 Y:2

Fler exempel

Här är några andra exempel som inte finns på MiniZinc-sajten eller i distributionen. Flera av dem är sådana jag brukar ha som standardproblem för att för att testa olika constraint-system vad gäller språk, performance och rent allmänt hur det är att arbeta med. T.ex. så kollade jag i höstas in AMPL (ett mycket trevligt system för "matematisk programming") men där var man i vissa fall tvungen att trixa ordentligt - i och för sig vedertagna och väl dokumenterade tricks - för att göra sådant såsom "all_different". Minizinc (och de flesta andra constraint system) har all_different implementerat som standard.

I Choco: Constraint Programming i Java gavs några exempel på problem som löstes i constraint programming-systemet Choco. Dessa har nu skrivits om i Minizinc. Som jämförelse länkas även till Choco-varianten.

* Planering av möbelflyttande, använder "global constraint" cumulative

furniture_moving.mzn (FurnitureMoving.java)

* Ett enkelt knapsack-problem (minimering)

knapsack.mzn (Knapsack.java)

* Least diff (minsta differensproblemet som beskrivs i ovanstående blogganteckning)

least_diff.mzn (LeastDiff2.java)

* Sesemans klosterproblem

seseman.mzn (Seseman.java). Se Sesemans matematiska klosterproblem samt lite Constraint Logic Programming för en förklaring av detta problem.

* set_covering_deployment.mzn

Implementation av exemplet på Set Covering Deployment för att optimera antal arméer i gamla romarriket. Problemet beskrivs i detalj i R.R. Rubalcaba Fractional Domination, Fractional Packings, and Fractional Isomorphisms of Graphs (PDF).

de Bruijn-sekvener och "arbiträra de Bruijn-sekvenser"

Jag har länge varit fascinerad att de Bruijn-sekvenserna och publicerat två (eller tre beroende på hur man räknar) webbaserade program:

- de Bruijn sequence, samma som Java Applet

- de Bruijn arbitrary sequences, där man använder "de Bruijn-egenskapen" men tillåter sekvenslängden bestäms av användaren.

Se respektive de Bruijn-sekvenser (portkodsproblemet) och de Bruijn-sekvenser av godtycklig längd för förklaringar av programmen.

Naturligtvis var detta en sak som skulle kodas i Minizinc. Första versionen av programmet byggde liksom webbversionen av "de Bruijn arbitrary sequences" på en speciell typ av graf som traverserades på ett visst sätt. Denna implementation var dock lite trixig att genereralisera till andra baser än n=2. Därefter skrevs en variant där man programmerar de Bruijn-egenskapen direkt i stället för att gå via en graf, vilket gjorde det hela mycket mer generellt och (oftast) snabbare.

Denna senare variant finns att beskåda i debruijn_binary.mzn. (Anledningen till att programmet heter "_binary" är bl.a. för att jag fick idén till implementationen några minuter efter jag kodat klart Gray-koder).

Exempelkörning
Problemet som jag kallar för 2/4/16 är base = 2, n = 4 (antal bitar att använda), m = 16 (längden på sekvensen). Programmet spottar ur sig lite olika typer av information:

- bin_code / binary_code: själva de Bruijn-sekvensen
- x är decimalrepresentationen av vektorerna som utgör sekvensen
- gcc (förkorting av global cardinality constraint) kontrollerar hur många olika siffror (0..base-1) som används. Det finns en begränsning att det måste vara exakt lika många förekomster av de olika siffrorna om det är matematiskt möjligt. Och det är just denna begränsning som gör problemet både intressant och tungt. I exemplet ser vi alltså att det finns 8 stycken 0:or och 8 stycken 1:or.
- sedan kommer listningen av "bit-representation" av vektorerna

n: 4 m: 16 base: 2 bin_code: [0, 0, 0, 0, 1, 0, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1] gcc: [8, 8] binary code: 0000100110101111 x (decimal representation): [0, 1, 2, 4, 9, 3, 6, 13, 10, 5, 11, 7, 15, 14, 12, 8] 0 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0 1 0 0 1 0 0 1 1 0 1 1 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1 1 0 1 1 1 1 1 1 1 1 1 1 0 1 1 0 0 1 0 0 0

Ett problem som är betydligt tyngre att lösa är 4/3/52, dvs bas=4 (dvs siffrorna 0, 1, 2 och 3 används), 3 "bitar" i varje tals vektor, samt en sekvenslängd på 52. Detta är så tungt så man inte kan använde solve satisfy utan måste använda sökheuristiker för att inte vänta förgäves på en lösning.

Genom experiment (föregånget av luskande i källkod och dokumentation hittades följande
solve :: int_search(x, "first_fail", "indomain_split", "credit(5,bbs(1))") satisfy

(Zinc-specen förklarar ingående vara parametrarna innebär, men det är helt enkelt lite olika metoder att traversera problemträdet.)

Den praktiska innebörden är att Eclipse-solvern hittar 1 lösning mycket snabbt, 65 lösningar på 5 sekunder (jag vet inte hur många olika lösningar som det total finns men det är väldigt många i alla fall). Med credit(4,bbs(2)) blir det 108 lösningar på 8 sekunder, credit(4,bbs(4)) hittar 1104 lösningar på 1:07 minuter etc.

En av dessa lösningar är följande
n: 3 m: 52 base: 4 bin_code: [0,0,2,0,0,3,0,1,0,1,1,0,2,1,0,3,1,1,1,2,0,1,2,1,1,3,0,2,2,0,2,3,0,3,2,0,3,3,1,2,2,1,2,3,1,3,3,2,2,3,3,3] gcc: [13,13,13,13] binary code: 0020030101102103111201211302202303203312212313322333 x (decimal representation): [2,8,32,3,12,49,4,17,5,20,18,9,36,19,13,53,21,22,24,33,6,25,37,23,28,50,10,40,34,11,44,51,14,56,35,15,61,54,26,41,38,27,45,55,31,62,58,43,47,63,60,48]Total time 0.320s cpu (0.040 setup + 0.280 search)

Tyvärr har varken Flatzinc eller fz givit någon lösning alls på detta problem (jag har låtit båda programmen stå minst en timme varderna men sedan tröttnade jag). Om man däremot tar bort kravet att det ska exakt samma antal förekomster av siffror i sekvensen löser även fz problemet snabbt (men minizinc gör det inte).

Olika solvers

För närvarande finns tre olika solvers, med olika för- och nackdelar.

* flatzinc
Det är denna solver som följer med i Minizinc-distributionen.

Fördelar:
- det största fördelen är att den finns med i distributionen och kan alltså användas direkt.

Brister:
- ger endast en lösning oavsett hur många lösningar som problemet har. Detta är för mig en mycket stor brist.
- klen vad gäller beräkning av stora tal. T.ex. klarar den inte av grocery.mzn eftersom det är för stora tal inblandade.
- verkar inte vara känslig för de olika heuristikerna

* Gecode/flatzinc (fz)
Gecode/Flatzinc.

Kräver att Gecode finns installerad. Gecode är ett snabbt open source constraint programming-system (skrivet i C++) och har flera intressanta exempel. Det finns även en Java-implementation ovanpå Gecode Gecode/J. Båda dessa är väl värda att bekanta sig med helt oavsett Minizinc.

Fördelar:
- ofta mycket snabb, ibland snabbare än Eclipse-solvern (även fast man har heuristiker som hjälper Eclipse-solvern)
- ger flera lösningar (alla!) om det finns (såvida man inte "heuristicerar" bort dem)
- summerande statistik som indikerar hur svårt problemet är att lösa

Nackdelar:
- min uppfattning är att fz inte är lika känslig för sök-heuristikerna som Eclipse-solvern vilket gör att den kan vara långsammare än Eclipse-solvern för vissa problem
- klarar inte av vissa typer av flyttalsberäkningar, t.ex. mortgage exemplet ovan.
- kan reagera konstigt på sök-heuristikerna
- man måste installera gecode

* ECLiPSe
Kräver ECLiPSe Constraint Programming System. Det är en variant av Prolog (min favoritvariant och som användes i Sesemans matematiska klosterproblem samt lite Constraint Logic Programming).

För tillfället krävs en utvecklingsversion eftersom Minizinc-stödet ännu inte är officiellt släppt. Eftersom sajten crosscoreop.com kan bete sig konstigt vid hämtande av stora filer är att rekommendera att man hämta filerna från en av speglarna t.ex. http://sunsite.informatik.rwth-aachen.de/ftp/pub/mirror/ECLiPSe-CLP/.

Dokumentation hur man använder Minizinc-modulen finns i library(minizinc).

Ett tips är även att studera ECLiPSe-predikatet search/6 som är inspirationskällan för sök-heuristiken i Minizinc.

Fördelar:
- liksom fz mycket snabbt och ger alla lösningar
- klarar av flyttalsberäkningar (såsom mortgage)

Nackdelar:
- vissa saker är inte implementerade, såsom vissa set_operationer.
- man måste installera ECLiPSe-systemet.

Buggar eller brister

Här är några brister antingen i de aktuella implementationerna eller saker som stör mig i designen av språket.

* Utskrifen är inte fullständigt i den existerande beta-versionen. Det är trixigt att skriva ut mer komplicerade strukturer (se exemplen). Det finns för närvarande inget sätt att villkora så att man bara ska skriva ut vissa element i en var-deklarerad array (såsom endast de element som är större än 0). Till viss del är det ett desginbeslut, möjligen kommer fix() att lösa några av dessa problem.

* Typningen. Personligen tycker jag inte om den strikta typningen av float och int (det är enligt design) som gör att man explicit måste sköta sådant. T.ex. görs '/' (division) endast på flyttal och det gör att vissa problem blir mycket svårare att lösa (såsom några av Integer Programming-pysslen). Det är inte alltid det går att använda div-operatorn (som f.ö. är buggig i fz) eller att (på ett enkelt sätt) skriva om problemet så det inte använder division.

* Det saknas en solver som använder metoder från linjär programmering/heltalsprogramming (såsom simplex-metoden). Det antyds att det finns sådana men de är ännu ej släppta. I och för sig har ECLiPSe-systemet någon form av stöd för eplex i sin Zincinterface-katalog, men det har jag inte fått att fungera ännu. Uppdatering ett halvt dygn senare:: Jodå, eplex funkar för vissa typer av problem såsom några av exempeln i examples-kataloge; queens_ip.mzn, min_cost.mzn, product_lp och multidimknapsack_simple. Får alltså kolla in det mer...

Länkar
Annat som kan vara intressant.

* Integer Programming Puzzles (programmering av lösningarna av Martin Chlond). Detta är en härlig samling "heltalspyssel" (dvs där lösningarna är heltal, eller kan ses som heltal). Send More Money, Least Diff är några andra exempel på sådana problem.

När jag satt med AMPL i höstas konverterade jag i stort sett samtliga dessa problem från XPress till AMPL, och har nu kodat om dessa till Minizinc. Tyvärr är det inte alla Minizinc-implementationer som ger resultat inom rimlig tid. Ett projekt i vardande är att hyfsa till dem och sedan lägga ut dem på sajten.

Jag tänkte här egentligen länka till en del annat som jag hållt på med sedan oktober förra året, såsom Excel, Open Office Calc, Linear Programming, AMPL, GLPK, matematisk programming, Operations Research, andra constraint programming-system etc, men det blir i så fall i separata postningar.

Posted by hakank at 09:33 EM Posted to Constraint Logic Programming | Comments (6)

april 18, 2006

Choco: Constraint Programming i Java

Bakgrund
Mitt intresse för Constraint Programming (CP) (som tidigare kallades Constraint Logic Programming, CLP) väcktes för ett antal år sedan strax efter en företagskamp (som kort beskrevs i Uppdaterat program: AnaCheck), där ett av uppdragen var följande matematiska pyssel:

Vilken är den minsta differensen man kan få mellan två tal om man måste använda samtliga siffror (0..9) exakt en gång?

Lösningen presenteras nedan.

Ungefär samtidigt stötte jag på Constraint (Logic) Programming och med detta och liknande pyssel i bakhuvudet, och blev väldigt fascinerad av programmeringsparadigmet. Kanske inte så förvånande eftersom många standardexempel är just matematiska pyssel.

Tanken är att man endast behöver skriva de problemspecifika villkoren (constraints), sedan får systemet lista ut bästa sättet att lösa problemet. Det finns många olika metoder och heuristiker för att lösa problemen, och ibland måste hjälpa till så att lösningen kommer denna sidan regnbågen eftersom vissa problem är mycket tunga.

Ett citat som ofta nämns i sammanhanget är Eugene C. Freuder (CONSTRAINTS, April 1997)

Constraint programming represents one of the closest approaches computer science has yet made to the Holy Grail of programming: the user states the problem, the computer solves it..

Prologbaserade system
I början arbetade jag mestadels med logikprogramspråket Prolog som "moderspråk", Sicstus Prolog samt ECLiPSe Constraint Programming System (det senare inte att förväxlas med utvecklingsmiljön med ungefär samma stavning).

Imperativa språk
Som komplement till de Prologbaserade systemen har jag letat efter mer imperativa - samt icke-kommersiella - moderspråk såsom Java, C, C++, Perl, Python, eftersom vissa saker är lättare att programmera med sådana språk (men ibland svårare) En av dessa implementationer Python-constraint och nämns i kommentarerna till Sesemans matematiska klosterproblem samt lite Constraint Logic Programming.

Choco
Så till det system jag har kollat i nyligen: det Java-baserade Choco. I slutet av anteckningen finns fler referenser.

Choco är snabbt och det har en stor mängd funktioner. Exemplen nedan är endast för "finita domäner" (löses med hjälp av heltal), men det finns även domäner med reella tal samt mängder.

Det är dock inte lika elegant att skriva constraints som i Sicstus/ECLiPSe, vilket vi nu kommer att titta på.

Minsta differensproblemet - en jämförelse av kodskrivning
För att tydliggöra skillnader och likheter mellan Choco och de Prologbaserade systemen visas hur minsta differensproblemet kan lösas i respektive system.

I ECLiPSe skriver man själva constraint-delen av problemet på följande sätt; i Sicstus Prolog skriver man snarlikt. Obs: koden är inte riktigt komplett att bara köra.
:-lib(fd), lib(fd_search), lib(fd_global),lib(fd_domain).



% ....

LD = [A,B,C,D,E,F,G,H,I,J], % deklarera de 10 variablerna

LD :: [0..9], % intervallet för variblerna, mellan 0 och 9

fd_global:alldifferent(LD),  % alla värden ska vara olika

%

% constraints

%

% A + B + C + D + E = F + G + H + I + J

X #= 10000*A+1000*B+100*C+10*D+E,

Y #= 10000*F+1000*G+100*H+10*I+J,

% differensen ska bli positiv

X #< Y,

% differensen

Diff #= Y - X,

% minimera differensen (Diff) samt heuristik för att hitta lösningen snabbt

minimize(search(LD,0,anti_first_fail,indomain_max,credit(64,bbs(15)),[]),Diff).

Elegant och lite magiskt, eller hur?

Motsvarande Choco-program är lite längre, främst eftersom det saknas syntaktiskt socker. Det går att pressa antalet rader (sådant har gjorts) men här görs en mer expressiv form för att jämförelsen ska bli tydligare. Programmet finns att ladda ner här nedan.

// Choco program



import choco.Problem;

import choco.*;

import choco.integer.*;

public class LeastDiff {

    public static void main(String[] args) {

        new LeastDiff().puzzle();

    }

    public void puzzle () {

       Problem pb = new Problem();

       // definiera variablerna A .. J så att dess värden är mellan 0 och 9

        IntDomainVar A = pb.makeEnumIntVar("A", 0, 9);

        IntDomainVar B = pb.makeEnumIntVar("B", 0, 9);

        IntDomainVar C = pb.makeEnumIntVar("C", 0, 9);

        IntDomainVar D = pb.makeEnumIntVar("D", 0, 9);

        IntDomainVar E = pb.makeEnumIntVar("E", 0, 9);

        IntDomainVar F = pb.makeEnumIntVar("F", 0, 9);

        IntDomainVar G = pb.makeEnumIntVar("G", 0, 9);

        IntDomainVar H = pb.makeEnumIntVar("H", 0, 9);

        IntDomainVar I = pb.makeEnumIntVar("I", 0, 9);

        IntDomainVar J = pb.makeEnumIntVar("J", 0, 9);

        IntDomainVar[] letters = {A,B,C,D,E,F,G,H,I,J};

        IntDomainVar Diff = pb.makeBoundIntVar("Diff", 0, 10000);

        // Temporära variabler

        IntDomainVar X = pb.makeBoundIntVar("X", 0, 100000);

        IntDomainVar Y = pb.makeBoundIntVar("Y", 0, 100000);

        // alla värden ska vara unika

        for (int i = 1; i <= 9; i++) {

            for (int j = 0; j <= 9; j++) {

                if (i==j) {

                    continue;

                }

                pb.post(pb.neq(letters[i], letters[j]));

            }

        }

        // X = A+B+C+D+E

        pb.post(pb.eq(X, pb.scalar(new int[]{10000, 1000, 100, 10, 1},

                                   new IntDomainVar[]{A,B,C,D,E})));

        // Y = F +G + H + I + J

        pb.post(pb.eq(Y, pb.scalar(new int[]{10000, 1000, 100, 10, 1},

                                   new IntDomainVar[]{F,G,H,I,J})));

        // Diff = X - Y

        pb.post(pb.eq(pb.minus(X, Y), Diff));

        // minimera skillnaden

        pb.minimize(Diff,false);

        // nu ska vi lösa problemet

        Solver s = pb.getSolver();

        pb.solve(true);

        // Skriv ut lösningen

        System.out.println("Result: "+ A.getVal() + B.getVal() + C.getVal() +D.getVal() + E.getVal() + " - " + F.getVal() + G.getVal() + H.getVal() + I.getVal() + J.getVal() + " = " + Diff.getVal() );

      } // end puzzle

} // end class

Lösningen som ges av dessa båda program är samma, nämligen
50123 - 49876 = 247

Några körbara (kompilerbara) Choco-program
Här är källkoden till några andra mindre Choco-program, varav några är standardproblem inom constraint programming. Choco-distributionen innehåller några andra.

LeastDiff2.java: Ovanstående exempel
FurnitureMoving.java: Planering av möbelflyttande, använder cumulative.
Knapsack.java: ett enkelt knapsack-problem (minimize)
Zebra.java: ett standardpyssel
Seseman.java: Choco-versionen av Sesemans matematiska klosterproblem

Se även
om Choco:
Choco: projektsidan på Sourceforge
Wiki
User guide
Choco API
Forum

om constraint programming
Roman Barták: On-line Guide to Constraint Programming
Roman Barták: Constraint Programming: In Pursuit of the Holy Grail (PDF)

tidigare skrivet om C(L)P
Sesemans matematiska klosterproblem samt lite Constraint Logic Programming
Automatisk "lösning" av Minesweeper i Mozart/Oz

JaCoP är ett annat Javabaserat system, utvecklat vid Lunds Universitet som man kan få tillgång till om man frågor någon av dess skapare. Har inte kollat in det så mycket ännu, men det verkar också trevligt.

Posted by hakank at 09:59 EM Posted to Constraint Logic Programming | Matematik | Pyssel | Comments (0) | TrackBack

november 04, 2005

Sesemans matematiska klosterproblem samt lite Constraint Logic Programming

Bengt O. Karlsson ställde igår en matematisk gåta: Ett aritmetiskt problem av Hans Jacob Seseman. Se även den omslutande anteckningen Sesemania (som avslutas med en personlig anmaning). [Uppdatering: Titeln på den nyss angivna anteckningen är felaktig och ska vara Sesemana, men felskrivningen upplevdes av Bengt som en nära-Freud-upplevelse. Och hur kan man underlåta att ge Bengt en sådan njutning? Därför står felstavningen kvar i sin ursprungliga - men alltså felaktiga - prakt. Se något mer i kommentarerna till Bengts Sesemana -artikel. I sanningens namn korrigerades först felet, men sedan korrigerades rättet och denna uppdatering skrev som ett förtydligande.]

Det var ett kul litet problem, och inte speciellt svårt att lösa. En av utmaningarna var att korrekt tolka gammelsvenskan för att förstå vad problemet egentligen bestod av. Försök gärna lösa problemet själv innan ni läser vidare eller läser kommentarerna till problemet.

Uppdatering 2
På begäran har programmet Seseman's Convent Problem (se nedan) nu även möjlighet att visa unika lösningar, eller - mer korrekt - samla lösningar som är lika vad gäller rotation, spegling etc. Denna unicifiering har gjorts i CGI-programmet, ursprungligen som ett analysstöd för att eventuellt senare göra sådant i CLP-programmet.

Problemet
Problemet består av 4 liknande delproblem där det gäller att givet ett visst antal personer i ett kloster (nunnor samt eventuellt "tillkomne Karlar") ska man placera ut dessa personer i rum så att vissa villkor uppfylls.

A, B, C, D, E, F, G, H betecknar klostrets olika rum. Rummet "_" används inte, forutom att presentera en fin kvadrat.
A B C D _ E F G H

Ett krav är att vissa rader/kolumner ska ha summan 9:
A + B + C = 9 A + D + F = 9 C + E + H = 9 F + G + H = 9

Ett annat krav är att totalantalet personer ska vara en av de fyra summorna (24, 28,20, 32), som man själv fick lista ut med lite enkelt aritmetik. Villkoret är alltså:

A + B+ C + D + E + F + G + H = Totalsumma

Notera att det inte står någonting om huruvida rum kan vara tomma eller ej (se nedan om detta).

I kommentarerna till problemet visades ett antal olika lösningar, och det visar sig att problemet inte är entydigt eftersom några delproblem har flera lösningar, varav några presenteras av Fredriik och Hakke (också en Håkan K) samt undertecknad (Håkan K).

Constraint Logic Programming
Men det finns fler lösningar än så.

Problemet löstes ursprungligen med penna och baksidan av ett papper, men efteråt skapades ett litet CLP-program (Constraint Logic Programming) för att generera de olika lösningarna, närmare bestämt i det Prolog-baserade programspråket ECLiPSe (Gratis att ladda ner, men man måste anhålla om en licens.)

ECLiPSe-programmet finns här. Den centrala funktionen i programmet innehåller i stort sett endast de matemaitksa uttrycken ovan.
seseman(Rowsum, Total, FirstNum, LD) :- LD = [A,B,C,D,E,F,G,H], % deklarera variablerna



        % FirstNum = 0: empty rooms allowed

        % FirstNum = 1: empty rooms not allowed

        LD :: [FirstNum..9],

        % Radsumma/Kolumnsumma

        A+B+C #= Rowsum,

        A+D+F #= Rowsum,

        C+E+H #= Rowsum,

        F+G+H #= Rowsum,

        % summan av alla tal = Total

        A+B+C+D+E+F+G+H #= Total,

labeling(LD).

Den magiska genereringen av giltiga lösningar enligt restriktionerna (constraints) hanteras av labeling.

För att köra programmet från kommandoraden anger man följande:
eclipse -b seseman.ecl 9 24 1 -e 'go.'

där 9 är radsumman, 24 totalsumman. Talet 1 är ett hack för att ange att inget rum får vara tomt (0 om rum får vara tomma). -e 'go' är anropet till funktionen go och -b anger filnamnet.

Lösningar och ett webb-program
Det skrevs även ett webb-program som kommunicerar med ECLiPSe-programmet: Seseman's Convent Problem (monastary är munkkloster, convent är nunnekloster). Detta program gör det också möjligt att ändra på parametrarna skulle man så önska leka lite.

T.ex. finns det 7 lösningar för totalsumma 20 om man inte tillåter tomma rum och hela 73 lösningar om tomma rum tillåts.

Notera att programmet inte tar hänsyn att två lösningar kan vara samma fast de är roterade, spegelvända etc. Uppdatering Jodå, det gör det nu.

För de fyra olika totalsummorna som angav i problemet förevisas här antalet lösningar och om rum får vara tomma eller ej:
24 personer, tomma rum tillåts ej: 85 lösningar
24 personer, tomma rum tillåts: 231 lösningar

Som problemet är formulerat finns det dock bara en korrekt lösning för första delproblemet (24 nunnor): samtliga rum innehåller vardera 3 nunnor.

28 personer, tomma rum tillåts ej: 35 lösningar
28 personer, tomma rum tillåts: 165 lösningar
20 personer, tomma rum tillåts ej: 7 lösningar
20 personer, tomma rum tillåts: 73 lösningar
32 personer, tomma rum tillåts ej: 1 lösning
32 personer, tomma rum tillåts: 35 lösningar

Programmet har dock kvar begränsningen att maximalt antal personer som får finnas i ett rum är 9. Vi kan väl säga att det beror på att jag vill vara snäll mot webbservern. Om man vill leka med större värden kan man ändra 9 till något annat (t.ex. Total) på denna rad:
LD :: [FirstNum..9],

Kommentarer
Jag har inte hittat någon ren matematisk lösning på problemet, men en sådan kanske kommer (av någon). Ovanstående program gör det i alla fall möjligt att empiriskt studera problemet. Uppdatering: Det finns en bok Sesemans problem som kanske innehålla slika lösningar.

Man kan möjligen misstänka att Fredrik nu kommer att skriva ett mycket elegantare Python-program för detta problem.

För den som vill läsa mer om Constraint Logic Programming kan rekommenderas Programming with Constraints av Kim Marriott och Peter Stuckey. Boken innehåller många exempel som finns att ladda ner.

Posted by hakank at 11:48 EM Posted to Constraint Logic Programming | Matematik | Program | Comments (12) | TrackBack

hakank.blogg

Anteckningar från en PopSci-junkie blandat med egna mundäna försök. Samt annat.