Constraint solvers are a useful tool to have in the toolbox. You can pull one off the shelf, but there is value in understanding how they work. To that end, I will explore implementing the AC-3 constraint solver using F#.

The field of Constraint Satisfaction Problems (CSP) can be pretty vast. The variety of solvers provide their own balance of benefits and approaches to a problem. To provide some focus, it is worth discussing the general approach of the AC-3 constraint solver algorithm. Before proceeding, I need to provide a couple definitions. A CSP consists of several components. It starts with variables. Those variables can have possible values (domain). Variables have relationships between each other (arc constraints). A constraint is ultimately just a function which defines valid combinations of values with respect to a set of variables.

It often helps to see how a problem is defined and how the components interact, so here is a simple example. Below defines three variables (A, B, C), all with their own set of possible values. Additionally, there are some constraints. A must be even, so its possible values are reduced from { 1, 2, 3 } to { 2 }. B must be odd, so it is reduced to { 1, 3 }. A must be less than B, so A is still { 2 } and B has to be { 3 } (since 1 will never be greater than any value in A, in this case 2). C must be greater than A, which means C is reduced to { 3, 4, 5, 6 } (1 and 2 will never be greater than 2). This is generally how the components interact. If this doesn’t quite click for you yet, bear with me, I have more explanations below that will help solidify where this is all going.

Variables:

A = { 1, 2, 3 }

B = { 1, 2, 3, 4 }

C = { 1, 2, 3, 4, 5, 6 }

Constraints:

A, even()

B, odd()

A, B, lessThan()

C, A, greaterThan()

The AC-3 algorithm makes two passes, one for unary constraints and another for binary constraints. These passes reduce the domain of variables, eliminating impossible values based on those constraints. Unary constraints are pretty straight forward, if a value in the domain fails the constraint (returns false), it is eliminated. Like the previous example, if “A must be even”, odd numbers are removed from A’s domain. Binary constraints are more involved. The same rules apply, but it is applied with respect to two variables. This has the property that constraints can have a cascading effect across variables and their domains; the algorithm needs a way to handle this. It uses a work queue. As a variable’s domain is modified, it’s arc neighbors are added onto the work queue. This ensures the necessary processing is performed as long as domains keep changing. At some point all variables’ domains are reduced as much as possible, and the work queue empties out. Once all of this is done, if a variable domain is empty, then the solve “fails”. There are no possible provided values for at least one of the variables that can adhere to the provided set of constraints. On the other hand, if each variable has at least one value in its domain, then the solution is considered arc consistent, and the reduced domains are provided back to the caller. With this brief description out of the way, I’ll dive right into the code and add more details as I move along. So, like any other F# program, I need some good types to define the problem, I’m also going to package the logic into a module.

1 | /// Perform AC-3 constraint solving |

Performing domain reduction based on the unary constraints is the first major task. Conceptually it is a relatively straightforward process. Process each constraint separately. For each variable, iterate through each value of it’s respective domain. Using the constraint, filter out values that won’t work. Wrap this all in some recursive calls, and return the reduced variable domains.

1 | /// Reduce a variable's domain based on unary constraints |

The second major task is processing the binary constraints. Since these functions define the interaction of two variables, it is a bit more involved. It works off a queue of variables. After pulling a variable off the queue, it does a domain reduction based on every binary constraint that applies to it. This means for each constraint, iterating through it’s possible values and a neighbor’s possible values; and removing impossible combinations. During this process, if it reduces it’s domain, then the algorithm puts all of it’s neighbors on the work queue. This is because if a variable’s domain is reduced, it is possible that arc-connected variables could now have their domains reduced further. It is a reasonably efficient method to continuously check all impacted arc constraints without processing more than it needs to.

1 | /// Get a variable's neighbors (id list) |

The solver puts all of the pieces together. It takes the variables, and runs them through a unary constraint reducer, then the binary constraint reducer. Once this is done it just needs to check for success. If any of the domains are empty, then there are no valid solutions. This is because during the reduction process it removes impossible values, leaving you with only possible values. An empty domain is a result of no possibly valid values based on the constraints.

1 | /// Solve AC-3 constraint problem for the set of unary and binary constraints, and the variable domains. |

Now that the building blocks are together, it is time to test a constraint satisfaction problem. For example purposes, I’ll keep it simple. There are 4 variables, all with the integer domain { 0, 1, 2, 3, 4, 5, 6, 7 8, 9, 10 }. For reference sake, I’ll call the first variable (index 0), v0; the second variable (index 1), v1, etc. For unary constraints, v0 & v1 must be even numbers; v3 must be an odd number. The combined binary constraints require that v0 < v1 < v2 < v3. Running `solve`

will apply the AC-3 constraint solver and return true/false (where true means it is arc consistent, false means it is not). If true, it also returns the [potentially] reduced variable domains based on arc consistency.

1 | let even x = x % 2 = 0 |

The results below show that is arc consistent (yay). They also show the reduced domains of the variables. This is a good time to dig into the details. For explanatory sake, I’ll focus on variable 0 (v0). First, it’s unary constraint requires it to be even. So immediately it’s domain has to be reduced to { 0, 2, 4, 6, 8, 10 }. Second, the complete set of binary constraints require v0 < v1 < v2 < v3. Working backwards, v3 (which has be be odd due to it’s unary constraint), has a maximum value of 9. This means the max of v2 is 8, and v1 is 7 (actually 6, since it has to be even). This means the maximum value of v0 is 4. So, the reduced domain for v0 is { 0, 2, 4 }, which we see below (perfect). This example is really simple, but it helps to show how the impact of arc constraints cascading between variables.

1 | true |

That was a good starting example, but it is time to test the solver a bit more. I will add an additional constraint between variables 1 & 3. It isn’t enough to be less than, but there must be a larger gap (x + 4) between them. The logic to reduce variable domains work as before, but some variables have been reduced even further. The results show that this not impacts the domains of 1 and 3, but variable 0 as well; variable 2 seems unphased by this additional constraint.

1 | let bc = |

These examples have been insightful, but failures teach too. Now it is time to take a look at a set of constraints that don’t work. The constraints up to this point set up a progression where variable 0 < 1 < 2 < 3. Adding a constraint that v3 must also be less than v0 induces a conflict. The constraint solver finds this discrepancy. The solver returns false, the real indicator; but the variable domains are empty as well (bad sign).

1 | let bc = |

These examples give a glimpse into the methodology of a constraint solver, specifically AC-3. This has been fun. I hope you enjoyed this small view into how F# can be used to build interesting things, like the AC-3 constraint solver. There is an endless source of interesting problems, and having powerful tools in your toolbox can go a long way. Until next time.