AC-3 Constraint Solving with F#

Read Time: 15 minutes

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
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
/// Perform AC-3 constraint solving
[<RequireQualifiedAccessAttribute>]
module Ac3 =
  /// Variable domain
  type Domain = int list
  /// Variable Id (for lookup in map)
  type Id = int
  /// Variables (key=id, value=domain)
  type Variables = Map<Id, Domain>
  /// List of unary constraints for variables (<variable id>, <constraint function>)
  type UnaryConstraints = (Id * (int -> bool)) list
  /// List of binary constraints for variables (<variable id1>, <variable id2>, <constraint function>)
  type BinaryConstraints = (Id * Id * (int -> int -> bool)) list

  /// Convert an informal list of variables to the Ac3.Variables type
  let listToVariables (variables: (int list) list) :Variables =
    variables
    |> List.mapi (fun i x -> (i, x))
    |> Map.ofList

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
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
/// Reduce a variable's domain based on unary constraints
/// Return the resulting set of Variables with updated domain(s)
let rec private ucReduce (uc: UnaryConstraints) (variables: Variables) :Variables =
  // Iterate through all unary constraints, for each impacted variable, update it's domain
  match uc with
  | h :: t ->
      let (id, f) = h
      let d' =
        variables.Item id
        |> List.filter f

      let variables' =
        variables
        |> Map.remove id
        |> Map.add id d'

      ucReduce t variables'
  | _ -> variables

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
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
/// Get a variable's neighbors (id list)
let private neighbors (bc: BinaryConstraints) (id: Id) :int list =
  // Get neighbors of a variable (this is based on the binary constraints)
  bc
  |> List.filter (fun (id1, id2, _) -> id1 = id || id2 = id)
  |> List.map (fun (id1, id2, _) -> if id1 = id then id2 else id1)
  |> List.distinct

/// Reduce a variable's domain for a specific variable set and function
/// Returns: (<domain changed>, <reduced domain>)
let private reduceDomain (variables: Variables) (bc: BinaryConstraints) (id: Id) :bool * Domain =
  // Get constraints associated with the variable (id)
  let relevantConstraints =
    bc
    |> List.filter (fun (id1, id2, _) -> id1 = id || id2 = id)

  // Starting variable domain
  let d = variables.Item id

  // Iterate through constraints, saving the variable's new domain into the state
  // The final result is the reduced domain for the variable (and whether it changed or not)
  let (_, d') =
    relevantConstraints
    |> List.mapFold
       (fun state c ->
         // Extract constraint parts
         let (id1, id2, f) = c 

         // Update the variable's domain based on contraint
         let d' =
           if id1 = id then
             // id1 is the variable we are processing (use state), iterate through domain values of id2)
             state
             |> List.filter (fun v1 -> (variables.Item id2)
                                       |> List.exists (fun v2 -> f v1 v2))
           else
             // id2 is the variable we are processing (use state), iterate through domain values of id1)
             state
             |> List.filter (fun v2 -> (variables.Item id1)
                                       |> List.exists (fun v1 -> f v1 v2))

         // I don't care about the individual item result, I only care about the state (d' is the updated state of the domain)
         (None, d'))
       d

  // Determine if the variable's domain is updated
  let changed = d.Length <> d'.Length
  (changed, d')


/// Reduce a variable's domain based on binary constraints
/// Return the resulting set of Variables with updated domain(s)
let private bcReduce (bc: BinaryConstraints) (variables: Variables) :Variables =
  /// Perform a recursive domain reduction based on a variable worklist
  let rec bcReduce' (variables: Variables) (workList: Id list) :Variables =
    match workList with
    | id :: t ->
        let (changed, d') = reduceDomain variables bc id

        if changed then
          // The variable's domain was changed, update the worklist and continue
          let variables' =
            variables |> Map.remove id |> Map.add id d'

          let workList' = List.concat [ neighbors bc id; t ]
          bcReduce' variables' workList'
        else
          // The variable's domain was not changed, continue with remaining worklist
          bcReduce' variables t
    | _ -> variables

  // Define the initial working list of variables to process
  let workList =
    bc
    |> List.map (fun (id1, _, _) -> id1)
    |> List.distinct

  // Perform the arc constraint reduction
  bcReduce' variables workList

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
2
3
4
5
6
7
8
9
10
11
12
/// Solve AC-3 constraint problem for the set of unary and binary constraints, and the variable domains.
let solve (uc: UnaryConstraints) (bc: BinaryConstraints) (variables: Variables) =
  // Apply unary, then binary constraints 
  let variables' = variables |> ucReduce uc |> bcReduce bc

  // If any of domains are empty, no success
  let success =
    variables'
    |> Map.exists (fun k v -> List.isEmpty v)
    |> not

  (success, variables')

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
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
let even x = x % 2 = 0
let odd x = x % 2 <> 0
let lessThan x y = x < y

let variables =
  [ [ 0 .. 10 ]
    [ 0 .. 10 ]
    [ 0 .. 10 ]
    [ 0 .. 10 ] ]
  |> Ac3.listToVariables

let uc =
  [ (0, even)
    (1, even)
    (3, odd) ]

let bc =
  [ (0, 1, lessThan)
    (1, 2, lessThan)
    (2, 3, lessThan) ]

let (success, reducedVariables) = Ac3.solve uc bc variables
printfn "%A" success
reducedVariables
|> Map.toList
|> List.iter (fun x -> printfn "%A" x)

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
2
3
4
5
true
(0, [0; 2; 4])
(1, [2; 4; 6])
(2, [3; 4; 5; 6; 7; 8])
(3, [5; 7; 9])

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
2
3
4
5
6
7
8
9
10
11
12
  let bc =
    [ (0, 1, lessThan)
      (1, 2, lessThan)
      (2, 3, lessThan)
      (1, 3, (fun x y -> x + 4 < y)) ]

// Results:
true
(0, [0; 2])
(1, [2; 4])
(2, [3; 4; 5; 6; 7; 8])
(3, [7; 9])

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
2
3
4
5
6
7
8
9
10
11
12
13
  let bc =
    [ (0, 1, lessThan)
      (1, 2, lessThan)
      (2, 3, lessThan)
      (1, 3, (fun x y -> x + 4 < y))
      (3, 0, lessThan) ]

// Results:
false
(0, [])
(1, [])
(2, [])
(3, [])

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.

Related Posts: