Main

March 22, 2010

Minion version 0.10 released

Minion version 0.10 has been released. From the News:
March 17, 2010. Minion 0.10 has been released.

Changelog:

  • Nauty is now included by default for automatic symmetry detection.
  • New features:
    • added watchvecexists_less constraint
    • added quick lexless constraint
    • added lightweight table constraint
    • new flag -instancestats that will give various properties about the instance
    • new flag -searchlimit to limit only time spent in search and not in preprocessing
  • Bugfixes:
    • time limits are now taken into account during preprocessing as well
    • some of the generators were getting old and have been updated
    • reification of unary constraints works properly now
    • set constraints on empty sets now work
    • several bugfixes for watched constraints
  • Misc improvements:
    • speed improvements and memory for the parser
    • reduced memory requirements
    • improved testing
    • tidier reimplementation of the search manager
    • bumped minimum Mac OSX version from 10.4 to 10.5

February 22, 2010

Tailor version 0.3.3 released

Andrea Rendl released version 0.3.3 of Tailor this Friday.

News in this version:

* select a dynamic variable ordering for solving in Minion (in the GUI)
* extended GUI
* several bugfixes

From the README file (in the distribution):

6. Limitations and Known Bugs
----------------------------------
The translator is still under development, so there are some limitations.
The following is not supported yet:
- decision variable arrays with 4 or more dimensions
- parameter arrays with 4 or more dimensions
- absolute value
- power with decision variable as exponent
- element constraint on 2-dimensional arrays

Translation to Gecode:
- no parameter arrays supported
- complicated quantified sums not supported

Translation to Flatzinc:
- not supported: multi-dimensional arrays
- no support for table, element, atmost, atleast, gcc
- no modulo, power, division


Also see: My Tailor page

October 31, 2009

Some new models, etc

The readers that follows me on Twitter (hakankj) have probably already has seen this, but here follows a list of models, etc, not yet blogged about.

MiniZinc: Different models

The following four models are translation of my Comet models: And here are some new models:

Nonogram related

A large 40x50 Nonogram problem instance in MiniZinc: nonogram_stack_overflow.dzn to be used with nonogram_create_automaton2.mzn model. The problem was mentioned in Stack Overflow thread Solving Nonograms (Picross). It is solved in under 1 second and 0 failures.

Today my Nonogram model nonogram_create_automaton2.mzn was included in the great Survey of Paint-by-Number Puzzle Solvers (created by Jan Wolter).

My MiniZinc model is described and analyzed here. I'm not at all surprised that it's slower compared to the other solvers; it was quite expected.

Some comments:
Assessment: Slow on more complex puzzles.

...

Results: Run times are not really all that impressive, especially since it is only looking for one solution, not for two like most of the other programs reviewed here. I don't know what the differences are between this and Lagerkvist's system, but this seems much slower in all cases, even though both are ultimately being run in the Gecode library.
Update 2009-11-01
I later realized two things:

1) That the mzn2fzn translator did not use the -G gecode flag, which means that Gecode/FlatZinc uses a decomposition of the regular constraint instead of Gecode's built in, which is really the heart in this model. The model is basically two things: build an automata for a pattern and then run regular on it.
2) When Jan compiled Gecode, he set off all optmization for comparison reason. This is quite unfortunate since Gecode is crafted with knowledge of the specific optimizations.

I there have run all problems by myself and see how well it would done (at least the ballpart figure) when using an "normal" optimized Gecode and with the -G gecode flag for mzn2fzn.

Explanation of the values:
Problem: Name of the problem instance
Runtime: The value of runtime from Gecode/FlatZinc solver
Solvetime: The value of solvetime from Gecode/FlatZinc solver
Failures: Number of failures:
Total time: The Unix time for running the complete problem, including the time of mzn2fzn (which was not included in the benchmark).
A "--" means that a solution was not reached in 10 minutes.
Problem Runtime Solvetime Failures Total time
Dancer 0.002 0.000 0 1.327s
Cat 0.009 0.002 0 0.965s
Skid 0.012 0.006 13 0.660s
Bucks 0.015 0.004 3 0.866s
Edge 0.008 0.005 25 0.447s
Smoke 0.011 0.004 5 0.963s
Knot 0.026 0.006 0 1.450s
Swing 0.059 0.012 0 1.028s
Mum 0.120 0.093 20 1.811s
Tragic 6:24.273 6:23.607 394841 6:28,10
Merka -- -- -- --
Petro 2.571 2.545 1738 4.071s
M&M 0.591 0.510 89 1.961s
Signed 1.074 1.004 929 2.461s
Hot -- -- -- --
Flag -- [lazy solver: 2 solutions in 10 seconds] -- -- --
Lion -- -- -- --

It's interesting to note that the Lazy solver finds some solutions quite fast for the "Flag" problem. However, there where no other big differences compared to Gecode/FlatZinc. I also tested the problems with JaCoP's FlatZinc solver which solved the problems in about the same time as Gecode/FlatZinc with no dramatic differences.

As mentioned above, the exact values is not really comparable to the benchmark values. But it should give an indication of the result when using -G gecode and a "normal" optimized Gecode.

Unfortunately, I cannot link to the specific models due to copyright issues, but they can all be downloaded from the page Web Paint-by-Number Puzzle Export.

(End update)

Update 2009-11-02
Jan Wolter now have rerun the tests of my solver with the -G gecode option, and the time is much more like mine in the table above. The analysis is quite different with an assessment of Pretty decent, and the following under Result:
...

When comparing this to other solvers, it's important to note that nonogram_create_automaton2.mzn contains only about 100 lines of code. From Kjellerstrand's blog, it is obvious that these 100 lines are the result of a lot of thought and experimentation, and a lot of experience with MiniZinc, but the Olšák solver is something like 2,500 lines and pbnsolve approaches 7,000. If you tried turning this into a fully useful tool rather than a technology demo, with input file parsers and such, it would get a lot bigger, but clearly the CSP approach has big advantages.

(End update 2)

Also, the Gecode nonogram solver is included in the survey: called Lagerkvist. I'm not sure when it was added to the survey. It use the latest version of Gecode, so it must have been quite recent.

Some comments:
Assessment: Pretty decent.

...

Puzzles with blank lines seem to cause the program to crash with a segmentation fault.

Otherwise it performs quite well. There seems to be about 0.02 seconds of overhead in all runs, so even simple puzzles take at least that long to run. Aside from that, it generally outperforms the Wilk solver. It's not quite in the first rank, especially considering that it was only finding one solution, not checking for uniqueness, but it's still pretty darn good.

...
I mailed Jan today about the -solutions n options in the Gecode related solvers (he tested my MiniZinc model with Gecode/FlatZinc), as well as some other comments about my model. Also, I will download the problems tested and play with them.

Tailor/Essence': Zebra puzzle

Suddenly I realized that there where no Zebra problem, neither at Andrea's or here. So here it is: zebra.eprime: Zebra puzzle.

Gecode: Words square problem

See Gecode: Modeling with Element for matrices -- revisited for an earlier discussion of this problem.

Thanks to Christian Schulte my Word square model is now much faster: word_square2.cpp.

From the comment in the model:
Christian Schulte suggested 
using branch strategy INT_VAL_SPLIT_MIN 
instead of INT_VAL_MAX .
This made an improvement for size 7 from
322 failures to 42 and from 1:16 minutes
to 10 seconds (for 1 solution).
 
Now it manage to solve a size 8 in a reasonable 
time (1:33 minutes and 1018 failures):
  abastral
  bichrome
  achiotes
  shippers
  troponin
  rotenone
  amerinds
  lessness
 
But wait, there's more!

In the SVN trunk version of Gecode, there is now a version of this model: examples/word-square.cpp where Christian Schulte and Mikael Zayenz Lagerkvist has done a great job of improving it (using a slighly smaller word list, though). It solves a size 8 problem in about 14 seconds. There is also two different approaches with different strengths, etc. I have great hopes that it will improved even further...

July 25, 2009

New Tailor version (v0.3.2) and My Essence'/Tailor page

Since I have not written much about Tailor before, here is a short presentation of the system:
TAILOR is a tool that facilitates modelling and solving constraint models. TAILOR's graphical user interface (GUI) allows the user to directly solve an Essence' problem model with either solver MINION or GECODE, and is hence especially aimed at people who are novices in constraint programming or have no experience with constraint solvers Minion and Gecode. Note that TAILOR is not intended to compare solvers, but to generate effective solver input from a solver-independent problem model.
...

TAILOR provides a command-line and an interactive graphical version. TAILOR is distributed as a Java .jar file and can easily be executed on every platform.
Tailor is developed by Andrea Rendl of University of St Andrews in Scotland, UK.

New version v0.3.2

A new Tailor version was released some days ago. From the NEWS:
July 15, 2009: NEW RELEASE : TAILOR v0.3.2 (bug-fixed update from July 19, 2009) New Features * New output format: Flatzinc (still limited though) * New GUI options: o Solve your model directly in TAILOR with solver Gecode by using the Gecode-Flatzinc interpreter * Extended Gecode Translation (still restricted though) * several bugfixes (especially with XCSP format)
The Flatzinc output format is especially interesting, since there are now a lot of different solvers for solving Essence' models. A later finding reveals that there may have to be some tweakings in the FlatZinc file for using it with other solvers than Gecode/FlatZinc, since the translation (tailoring) is done explicitly for Gecode/FlatZinc.

Also, right now Tailor cannot generate FlatZinc files when the Essence' model contains multi dimensional arrays (matrices), but - as I understand it - this may come quite soon.

One should note that in Essence' it is not possible to stating search heuristics options. But it's quite easy to manually change that for the generated FlatZinc models (or, as I probably will do: make a program doing that). For the Minion solver there is a -varorder switch that change the variables order, but "[t]his flag is experimental and minion's default ordering might be faster" (to quote the help for the switch).

This can be examplified by the Calculs d'enfer puzzle, a minimizing alphametic puzzle. This is very slow for both Gecode/FlatZinc and Minion using the default solver settings. These remedies makes it much faster:
* FlatZinc: change (in the FlatZinc file) the solver clause to solve :: int_search(A, first_fail, indomain, complete) minimize a_max;
* Minion: Run Minion as minion -varorder srf calculs_d_enfer.eprime.minion

Update: In my simple wrapper program eprime.pl (Perl program) which I tend to use, I have now added support for "annotations" in the Eseence' file which handle these things The model now contains these two lines::
$ MINION :: -varorder srf
$ FLATZINC:: solve :: int_search(A, first_fail, indomain_min, complete) minimize a_max;
The MINION annotation simply adds -varorder srf to the argument list of the minion program, and the FLATZINC annotation replaces the default line solve satisfy, with the int_search parameter.
Note: The program eprime.pl is not very tidy but may be obtainable upon request. (end of update)

Some notes about the Essence' language

The language used in Tailor is Essence' (it also supports XCSP files ). This is a simplified version of ESSENCE (no prime). For more about Essence' see Modelling with Essence' and the examples. Also, see the Tailor tutorial.

Essence' is similiar to MiniZinc in its high-level approach, and it was very easy to translate (most of) the MiniZinc models to Essence'.

Example: Minesweeper

As an example, here is the complete model of Minesweeper (the param lines are usually in a separate parameter file):
ESSENCE' 1.0
letting X be -1 $ the unknowns
letting AB be domain int(-1..1)
given r : int $ rows
given c : int $ column
$ encoding: -1 for unknown, >= 0 for number of mines in the neighbourhood
given game : matrix indexed by [int(1..r),int(1..c)] of int(-1..8)

find mines : matrix indexed by [int(1..r),int(1..c)] of int(0..1)

$ Problem from Gecode/examples/minesweeper.cc  problem 0
param r be 6
param c be 6
param game be [
   [-1,-1,2,-1,3,-1],
   [2,-1,-1,-1,-1,-1],
   [-1,-1,2,4,-1,3],
   [1,-1,3,4,-1,-1],
   [-1,-1,-1,-1,-1,3],
   [-1,3,-1,3,-1,-1]
   ]

forall i : int(1..r) . forall j : int(1..c) . 
  (     
   ((game[i,j] > -1) => (mines[i,j] = 0)) /\
   ((mines[i,j] = 1) => (game[i,j] = -1)) /\
   (
    (game[i,j] >= 0 ) =>
      (
       game[i,j] = sum a,b : AB .
          ( (i+a > 0)  /\ (j+b > 0) /\
            (i+a <= r) /\ (j+b <= c)) * (mines[i+a,j+b])
      )
    )
  )
Compared to the MiniZinc model minesweeper.mzn, we can see some things:
* The where clause is missing in Essence'. Instead a condition is used, here: (game[i,j] >= 0 ) =>.
* Also, the syntax of the forall statement is somewhat different.
Otherwise it's quite similiar.

One feature I like it the "array slice" operator (e.g. x[i,..]) which slices all the columns of row i. For example, in quasigroup_completion.eprime the following to constraints makes a matrix a lating square:
forall i : int(1..n) .
   alldiff(x[i,..]),

forall j : int(1..n) .
   alldiff(x[..,j])
One of the biggest differences between Essence' and MiniZinc languages (and all the other constraint programming systems I've tested so far) is, in my view, that Essence' don't support predicates (user defined functions), which can make the model less clear; predicates (say, decomposed global constraints) is a nice way of structuring models.

Array access in Essence'

One of the things I test when learning a new system is how to access matrices consisting of decision variable indexed by another decision variables. I wrote about this in Learning constraint programming - part II: Modeling with the Element constraint and Learning Constraint Programming IV: Logical constraints: Who killed Agatha? revisited.

There was no problem at all in Essence' of modeling the Agatha problem: The model is here who_killed_agatha.eprime. The following two constraints, which has been a problem in some other systems, worked as a charm in the Essence' model:
hates[the_killer, the_victim] = 1,
richer[the_killer, the_victim] = 0,
The crossword problem, however, is another story. I used exactly the same principle as in the MiniZinc model crossword.mzn, but the Essence' constraint
A[E1, 3] = A[E2, 1]
give the following error: Flattening error. Cannot translate array element with non-constant element index:A[E3,5].

Well, this is consistent with the section 6. Limitations and Known Bugs in the README file of the distribution:
The translator is still under development, so there are some limitations. 
The following is not supported yet:
- decision variable arrays with 4 or more dimensions
- parameter arrays with 4 or more dimensions
- absolute value
- power with decision variable as exponent
- element constraint on 2-dimensional arrays

Translation to Gecode:
- no parameter arrays supported
- complicated quantified sums not supported

Translation to Flatzinc:
- not supported: multi-dimensional arrays
- no support for table, element, atmost, atleast, gcc
- no modulo, power, division

My Essence'/Tailor page

Inspired by this new Tailor release, I implemented some Essence' models which now are collected at My Essence'/Tailor page. As usual, I started with my "learning models", and implemented almost all of them.

Here are the Essence' models (and related parameter/data files) as of writing: I have also updated Common constraint programming problems to include these Essence' models.

February 18, 2009

Minion version 0.8 released

Version 0.8 of Minion is released.

Minion is presented in the following way


MINION is a new constraint solver, which is very fast and scales well as problem size increases. Empirical results on standard benchmarks show orders of magnitude performance gains over state-of-the-art constraint toolkits. These gains increase with problem size --- MINION delivers scalable constraint solving.

MINION is a general-purpose constraint solver, with an expressive input language based on the common constraint modelling device of matrix models. Focussing on matrix models supports a lean, highly-optimised implementation. This contrasts with current constraint toolkits, which, in order to provide ever more modelling and solving options, have become progressively more complex at the cost of both performance and usability.

MINION is a black box from the user point of view, deliberately providing few options. This, combined with its raw speed, makes MINION a substantial step towards Puget's `Model and Run' constraint solving paradigm.

From the relase notes for version 0.8:


Users who use pre-compiled binaries should find any existing problem
files run the same as before. Building from source has changed
substantially, with Minion now requiring both the 'cmake' build system
and 'boost' C++ library. Full instructions are included in the source
package.

[a lot of bug fixes]

Note that Tailor is not part of the standard Minion distribution anymore; it is
released separately.

Tailor can be downloaded here.

January 05, 2009

Tom Schrijvers: "Monadic Constraint Programming" (in Haskell)

Tom Schrijvers presents in the blog post Monadic Constraint Programming a draft version of the paper Monadic Constraint Programming written by him, Peter Stuckey, and Philip Wadler:


A constraint programming system combines two essential components: a constraint solver and a search engine. The constraint solver reasons about satisfiability of conjunctions of constraints, and the search engine controls the search for solutions by iteratively exploring a disjunctive search tree defined by the constraint program. In this paper we give a monadic definition of constraint programming where the solver is defined as a monad threaded through the monadic search tree. We are then able to define search and search strategies as first class objects that can themselves be built or extended by composable search transformers. Search transformers give a powerful and unifying approach to viewing search in constraint programming, and the resulting constraint programming system is first class and extremely flexible.


Prototype code in Haskell can be downloaded here.

December 29, 2008

Welcome to my My Constraint Programming Blog

Welcome to my My Constraint Programming Blog!

This is an extension of my "normal" swedish blog hakank.blogg, and will contain news etc about constraint programming and related paradigms. It will also link to my newly written constraint programming models.

As stated (in swedish) in Constraint programming-nyheter samt nya MiniZinc-modeller (~ Constraint programming news and some new MiniZinc models) the target group for this kind of things (especially in swedish) is quite small. Hence this new blog, and in english.

Some links as introduction to what I have done so far:
* My Constraint Programming page

* My MiniZinc page
* My JaCoP page
* My Choco page

The latter three pages contains information about the systems and some models. I regard the MiniZinc page as my main constraint programming page, since MiniZinc is - as time of writing - my favorite system.

If you know swedish, you may also read the Constraint programming category at hakank.blogg.


News


And we start with some new MiniZinc models written this weekend.

Three Rosetta Code programs, just to test the limits of MiniZinc.

* 99_bottles_of_beer.mzn: 99 bottles of beer
* knapsack_problem.mzn: Knapsack problem
* pyramid_of_numbers.mzn: Pyramid of numbers

And then an operations research model.
* sportsScheduling.mzn Sport scheduling, using channeling for symmetry breaking. I didn't found out how to generate the channeling matrix automatically, so a Perl one-line is used instead (contained in the model). It was inspired by the Essence' model sportsScheduling.eprime from the Tailor (Minion) distribution.