Constraint-Satisfaction Problems with MiniZinc + Gecode

Constraint-Satisfaction Problems (CSPs) are a type of problem in computer science. They are made of variables, possible values, and constraints on those values. Many problems, like graph theory, type inference, and puzzle-solving, work as CSPs. <!--more--> In this tutorial, we will use MiniZinc and Gecode to model and solve a simple graph-coloring problem. MiniZinc is a programming language built for CSPs. Gecode is a "solver" program for CSPs.

Prerequisites #

This tutorial does not assume existing knowledge about CSPs. We cover the basics of CSPs at the beginning. Yet it will help if you already know some programming basics (like types and constants). This makes some of the MiniZinc language easier to understand.

Constraint-Satisfaction basics #

A Constraint-Satisfaction Problem is composed of 3 sets, 3 groups of items with no repeats in a set. These groups are X, the variables; D, the domains, and C, the constraints.

Defining a CSP #

The first set, X, is the set of variables, which are like programming variables. These can be x, y, z, x₁, x₂, or any other variables. Each variable can take on a value from its domain, which is found in the second set D.

A domain is, itself, a set of (a finite number of) possible values for a corresponding variable.

So if X={x₁, x₂, x₂} is your set of variables, then D={d₁, d₂, d₃} is your set of domains.

The ith variable in X, x_i, can be a value from the set d_i.

The final set, C, is the set of constraints on the values of the variables.

A constraint is some rule placed on the value of one or more variables.

If C={x₁ + x₂ = 3}, we can only pick values from d₁ and d₂ that make x₁ and x₂ add up to 3.

Putting this all together, we could define a simple CSP as follows:

X={x, y}

All domains are the same: d_x=d_y={2,3}.

This means x can be either 2 or 3, and y can be either 2 or 3.

The only constraint: x+y > 4

The "solutions" to these CSP are the possible values of x and y that make the constraint true, given the available domain values.

One solution would be if x=2 and y=3. If we set the values as x=2 and y=2, this would not be a solution, since 2+2 = 4, which is not greater than 4. Those values violate the constraint, so they cannot be a solution.

For more theoretical details, you can check Enric Rodríguez-Carbonell's notes on the subject.

CSP applications #

You'll find that many problems lend themselves to CSP solutions. They have objects (variables) with possible values (domains) and rules about their interactions (constraints).

One example is any problem involving a graph, or a network of nodes.

In the graph below, there are 5 nodes, and several connections between them. Each connection has a "cost", given by its number. In real life, each node could be a city (city 1, city 2, etc.), and each connection a road with a cost. So the road from city 1 to city 2 costs $2 toll (or takes 2 hours) to drive on.

Image source:Wikimedia Commons

You want to visit every city exactly once (no repeated nodes). You also want the lowest travel cost (smallest sum of connection-costs). How do you solve the problem?

You can convert the information about the graph into a Constraint-Satisfaction Problem. The variables could be the order in which you visit each city (where x_i is the ith city visited). The domains can be the cities.

The constraints would include:

• "Lower the cost of the path traveled on as much as possible."
• "You can't visit the same city twice."
• "You have to visit every city."

And so on. Constraints would be written with corresponding equations.

This is a version of the traveling salesman problem. Such problems crop up in GPS navigation; Google Maps wants to find the quickest route from your house to your workplace.

Other problems break down to CSP components in a similar fashion, including "schedule these jobs to minimize wasted time", and "figure out if this data is a number or a letter".

Our example problem: Map-coloring #

Map-coloring is easy to convert into a Constraint-Satisfaction Problem. Here, you want to color countries or states on a map, without coloring two touching states with the same color. We will find such a coloring style for the map below of the United States. We only look at the continental 48 states only, so we will exclude Alaska, Hawaii, and the territories.

Image source: Wikimedia Commons

Our coloring can be rewritten as a CSP, where the constraint is that any states that touch each other cannot be the same color. Texas (TX) cannot be green if Louisiana (LA) is green. So we need at least two colors for a valid map-coloring. Doing this by trial-and-error is hard, while CSP modeling makes it easy.

CSP tools for pros #

Some basic CSP tools exist for common languages, like Python and JavaScript. But, the basic options don't work well to model and solve large, complex problems. Specialized tools can handle those, and also speed up CSP solving, as they're optimized for that purpose alone.

That is why we will use MiniZinc and Gecode in our Constraint-Satisfaction Problem. MiniZinc is a language designed for constraint-modeling. Gecode is a solver, a separate module that finds values for the variables to satisfy the constraints.

Installing MiniZinc #

To get started, we have to download and install MiniZinc. MiniZinc is best used with the (free, open-source) MiniZinc IDE, which comes with Gecode, other solvers, and a MiniZinc compiler.

Go to the MiniZinc downloads page and click the recommended installer that matches your operating system.

If you don't see your OS, or need a 32-bit version, look for an alternative release here or here.

In this tutorial, we use MiniZinc 2.5.3 on Windows 10.

Once you've downloaded the installer (named something like MiniZincIDE-2.5.3-bundled-setup-win64.exe in your Downloads folder), click to run it.

If you're on Windows, and got a "Windows protected your PC" popup, click "More info" and then "Run Anyway". Follow the installer's prompts (the defaults are fine, accept the agreement). Click "Install" and then "Finish".

A window will pop up asking for automatic-update checking. Click "No" unless you're okay with them sending anonymized statistics to Google Analytics.

Finally, you will see an untitled MiniZinc project that looks something like this:

Note that the "Solver configuration" in the top right corner says "Gecode 6.3.0". That's exactly what we want, as we're using Gecode as our solver.

If that box says something else, click it and select a "Gecode" option from the drop-down menu. MiniZinc does support custom solvers, which you can learn more about here.

Setting up the problem #

MiniZinc (the language) is used to model Constraint-Satisfaction Problems. It works like many languages you may have already encountered. We'll start with a integer, the parameter num_colors.

It represents the number of colors we want to use on our problem. We can't change this number (it's a constant), since it will constrain how many colors we can use.

int: num_colors = 4;

% this is a comment
% the rest of the CSP will go here

The four-color theorem tells us we can color any map with no more than 4 different colors. We'll solve our map-coloring problem for 4 colors, and later see if we can do so with fewer colors.

Our code is partly based on a simpler map-coloring example in the MiniZinc documentation. We also took inspiration from Listing 2.2.2 in other MiniZinc documentation, and a basic traveling-salesman example from the University of Glasgow. Curious readers can investigate these further.

Now, we put a MiniZinc "solve" command at the end of our code, to make it look like this:

int: num_colors = 4;

% this is a comment
% the rest of the CSP will go here

solve satisfy;

The "satisfy" keyword tells MiniZinc that we need some kind of solution to the problem, not the "best" solution.

Press Ctrl-S or click File>Save to save the file. Call it us_map.mzn, as .mzn files are MiniZinc's code format.

Variables and domains #

Now, we need our variables and domains. Each state is a variable, we color it with one of 4 colors. Each color is actually an integer (from 1-4 inclusive). It doesn't matter which color each integer represents, as long as they are different.

In MiniZinc, a variable is defined like var domain: identifier;. The domain is the range of values that the variable (named by the identifier) can take on.

We can define Texas as var 1..num_colors: TX;.This says "TX is a variable that can have a value from 1 to num_colors, inclusive".

However, we don't want to type out this declaration for every variable. Instead of each state being a color variable, we will use an enum (constant list) of state names, and an array of their color values. This will make the final results more legible, and allows other states to be added easily.

Remove the commented lines (starting with %), since we'll insert the rest of our code there.

The enum will enumerate all the state abbreviations:

enum States = {AL, AK, AZ, AR, CA, CO, CT, DC, DE, FL, GA, 
          HI, ID, IL, IN, IA, KS, KY, LA, ME, MD, 
          MA, MI, MN, MS, MO, MT, NE, NV, NH, NJ, 
          NM, NY, NC, ND, OH, OK, OR, PA, RI, SC, 
          SD, TN, TX, UT, VT, VA, WA, WV, WI, WY};

Each of those state abbreviations will denote an integer in our colors array:

array[States] of var 1..num_colors: colors;

An array declaration in MiniZinc can be structured as array[keys or size] of type: arrayname. So our state-color array is named "colors". The "key" value (name of each item) is based on the variables in the States enum.

Each color is typed like our previous single-variable, var 1..num_colors. The key can also be an index range of items (0..2).

Constraints #

Now that we have our variables, let's set constraints.

If we had continued our earlier practice of using lone variables, the Texas constraints would be:

constraint TX != LA;
constraint TX != OK;
constraint TX != AR;
constraint TX != NM;

Texas (TX) touches Louisiana (LA), so we cannot color them the same color. This means the value (integer) for TX cannot be the same as the value of LA.

Because we use a colors array, we would write these constraints by accessing array items:

constraint colors[TX] != colors[LA];
constraint colors[TX] != colors[OK];
constraint colors[TX] != colors[AR];
constraint colors[TX] != colors[NM];

We've provided the full U.S. state constraints file, all_state_touching_constraints.mzn.

It contains the full list of state-touching constraints. Download that file by clicking the link and pressing Ctrl-S (or clicking File>Save in your browser).

Then, click and drag it into the folder you saved us_map.mzn in. Import this list of constraints into MiniZinc, to let the main file use the constraints.

Your code should look like this:

int: num_colors = 4;

enum States = {AL, AZ, AR, CA, CO, CT, DC, DE, FL, GA, 
          ID, IL, IN, IA, KS, KY, LA, ME, MD, 
          MA, MI, MN, MS, MO, MT, NE, NV, NH, NJ, 
          NM, NY, NC, ND, OH, OK, OR, PA, RI, SC, 
          SD, TN, TX, UT, VT, VA, WA, WV, WI, WY};

array[States] of var 1..num_colors: colors;

include "all_state_touching_constraints.mzn";

solve satisfy;

Finally, we want to see our solution in full. We'll use the "output" command, which can iterate through the States enum and print out the data. At the very end of your code, add this line:

output [ "\(s) = \(colors[s]);\n" | s in States ];

The \(variable) syntax lets you output strings of the variables. The \(s) is the state code, the \(colors[s]) is the color number assigned, and | s in States means "for every state s in the States enum".

Solving the model with Gecode #

Satisfying the problem #

Finally, we can solve the model with Gecode. Make sure the "Solver configuration" is set to "Gecode 6.3.0", and click on the "Run" button (or press Ctrl-R) to run our code.

You should get an output at the bottom of the IDE, looking like this:

AL = 3;
AZ = 1;
AR = 3;
CA = 2;
CO = 2;
CT = 3;
DC = 1;
DE = 1;
FL = 1;
GA = 2;
ID = 2;
IL = 1;
IN = 2;
IA = 3;
KS = 3;
KY = 3;
LA = 1;
ME = 2;
MD = 3;
MA = 2;
MI = 1;
MN = 4;
MS = 2;
MO = 2;
MT = 3;
NE = 4;
NV = 4;
NH = 1;
NJ = 3;
NM = 4;
NY = 1;
NC = 3;
ND = 1;
OH = 4;
OK = 1;
OR = 1;
PA = 2;
RI = 1;
SC = 1;
SD = 2;
TN = 1;
TX = 2;
UT = 3;
VT = 3;
VA = 2;
WA = 3;
WV = 1;
WI = 2;
WY = 1;
----------
Finished in 178msec

To read this output, we see the state's abbreviation on the left, and its color-number on the right. So WY (Wyoming) and TN (Tennessee) are the same color.

Optimizing the problem #

Now, what if you not only wanted to solve this problem, but to solve it with the minimum number of colors? MiniZinc makes this easy, requiring only 4 minor changes:

1. Move and changenum_colors to be a variable, representing the biggest color-number in the array. So we change its declaration to var int: num_colors = max(colors);, the biggest color-number in the colors array. We want to minimize this value, so it's not a constant parameter.
2. Change the colors array value type to be an int from 1 to 4. Because num_colors is unassigned, we cannot use it in ranges, but we know we'll use at least 1 color and no more than 4 colors (by the four-color theorem).
3. Change the "solve" statement to solve minimize num_colors;. This will tell Gecode to satisfy the problem in the way that makes num_colors as small as possible.
4. Add another "output" statement at the end of the file, to tell us how many colors we needed, printing out num_colors's value.

Your final code should look like this:

enum States = {AL, AZ, AR, CA, CO, CT, DC, DE, FL, GA, 
          ID, IL, IN, IA, KS, KY, LA, ME, MD, 
          MA, MI, MN, MS, MO, MT, NE, NV, NH, NJ, 
          NM, NY, NC, ND, OH, OK, OR, PA, RI, SC, 
          SD, TN, TX, UT, VT, VA, WA, WV, WI, WY};

array[States] of var 1..4: colors;

include "all_state_touching_constraints.mzn";

var int: num_colors = max(colors);

solve minimize num_colors;

output [ "\(s) = \(colors[s]);\n" | s in States ];
output [ "We only needed \(num_colors) colors for this problem." ];

Click "Run" or Ctrl-R again, and the output is...

Running us_map.mzn
AL = 3;
AZ = 1;
AR = 3;
CA = 2;
CO = 2;
CT = 3;
DC = 1;
DE = 1;
FL = 1;
GA = 2;
ID = 2;
IL = 1;
IN = 2;
IA = 3;
KS = 3;
KY = 3;
LA = 1;
ME = 2;
MD = 3;
MA = 2;
MI = 1;
MN = 4;
MS = 2;
MO = 2;
MT = 3;
NE = 4;
NV = 4;
NH = 1;
NJ = 3;
NM = 4;
NY = 1;
NC = 3;
ND = 1;
OH = 4;
OK = 1;
OR = 1;
PA = 2;
RI = 1;
SC = 1;
SD = 2;
TN = 1;
TX = 2;
UT = 3;
VT = 3;
VA = 2;
WA = 3;
WV = 1;
WI = 2;
WY = 1;
We only needed 4 colors for this problem.
----------
==========
Finished in 174msec

... identical! As it turns out, you still need 4 colors for the United States map.

Conclusion #

Congratulations! You've learned about and implemented a Constraint-Satisfaction Problem in MiniZinc, and solved it with Gecode.

If you want to make more flexible or complex models (that you can run from the command line!), MiniZinc has several tutorials for these advanced features.

---

Peer Review Contributions by: Mike White