AC-3 Constraint Solving with Zig

Read Time: 12 minutes

Constraint solvers are a good tool to have in the toolbox. If this sounds like a familar beat, it should. Today I’m revisiting the AC-3 constraint solver I had previously written in F#, but this time I’ll be using Zig as a continued learning adventure.

A bit of a Constraint Satisfaction Problems (CSP) refresher may be in order. The AC-3 constraint solver is used to determine arc consistency between a set of variables and their possible values, with respect to a set of constraints. What does this mean in practice? It is provided a series of variables, each with their own domain of possible values. They also have relationships with other variables (arc constraints). Constraints come in two forms. Some are unary (i.e. all domain values for a variable must adhere to a constraint). Others are binary (i.e. a relationship between domain values in two variables must adhere to a constraint). Ultimately a constraint is just a function that takes one or two variables and returns a boolean. The AC-3 solver takes this information and reduces the domains of the variables so that each value in a domain has the possibility of being valid. This does not mean every combination of all values are valid. It just means that each one of the values could be valid, depending on other values selected in other 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.

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()

With the definition of the problem in place, its time to do some evaluation. 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). Below is the reduced domains for each variable.

Variables Reduced:
A = { 2 }
B = { 3 }
C = { 3, 4, 5, 6 }

Digging into definitions a bit more. A unary constraint is a function that takes a value, performs a calculation, then returns true if it succeeds and false if it doesn’t. 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. The pass/fail criteria is slightly more involved. When running a constraint check, if there is at least one value in variable2’s domain, when paired with a specific value in variable1, then the variable1 value is considered valid. If not, then that value is removed from variable1’s domain. Since variables can have multiple constraints, there can be 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 any 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.

Here is where I deviate from my previous post. If you want to see the implementation, you can find the code in my repo. Or if you’re more interested in an algorithm break down, checkout out my other post. This felt like a good opportunity to not only learn how to implement this in Zig, but how to package it in a module So the first step is to create an application. The second is to include the ac3 module. Following the steps below the module can be added to the project. As a note, this library currently targets Zig 0.13.0.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
# Create Zig application files and some default structure.
zig init

# Run 
zig fetch --save git+https://github.com/0x6a62/constraint-solving.git

# Add to build.zig:
const constraint_solving = b.dependency("constraint-solving", .{
    .target = target,
    .optimize = optimize,
});
exe.root_module.addImport("ac3", constraint_solving.module("ac3"));

# Use in code
const ac3 = @import("ac3");

Now that the setup is in place, it is time to put a simple constraint satisfaction problem together. I’ll break the components of the problem here. Here are the constraint functions. These couple be anything, as long as they conform to i32 -> bool or i32 -> i32 -> bool.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// Unary constraint functions

pub fn isEven(x: i32) bool {
    return @mod(x, 2) == 0;
}

fn isOdd(x: i32) bool {
    return !(isEven(x));
}

fn isPowerOfTwo(x: i32) bool {
    return std.math.isPowerOfTwo(x);
}

// Binary contraint functions

fn isLessThan(x: i32, y: i32) bool {
    return x < y;
}

fn isSumEven(x: i32, y: i32) bool {
    return @rem(x + y, 2) == 0;
}

The problem itself has five variables along with seven constraints. The variables with their respect domains are shown below. As a note, the domains must must be vars, since they are mutated (reduced) during the contraint processing steps.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
var aDomain = [_]i32{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 };
const a = ac3.Variable.init(.{ .name = "a", .domain = &aDomain, });

var bDomain = [_]i32{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 };
const b = ac3.Variable.init(.{ .name = "b", .domain = &bDomain, });

var cDomain = [_]i32{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 };
const c = ac3.Variable.init(.{ .name = "c", .domain = &cDomain, });

var dDomain = [_]i32{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 };
const d = ac3.Variable.init(.{ .name = "d", .domain = &dDomain, });

var eDomain = [_]i32{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 };
const e = ac3.Variable.init(.{ .name = "e", .domain = &eDomain, });

var variables = [_]ac3.Variable{ a, b, c, d, e };

The heart of the problem are the constraints. “a” must be even. “b” must be odd. “c” must be a power of two. Also, “a < b”. “b + d” must be even (there are two rules for this so b+d = d+b). Lastly, “e < a”. Below is how the constraints are represented.

1
2
3
4
5
6
7
8
9
10
11
12
const unary_constraints = [_]ac3.UnaryConstraint{
    ac3.UnaryConstraint{ .name = "a", .constraint = &isEven },
    ac3.UnaryConstraint{ .name = "b", .constraint = &isOdd },
    ac3.UnaryConstraint{ .name = "c", .constraint = &isPowerOfTwo },
};

const binary_constraints = [_]ac3.BinaryConstraint{
    ac3.BinaryConstraint{ .name1 = "a", .name2 = "b", .constraint = &isLessThan },
    ac3.BinaryConstraint{ .name1 = "b", .name2 = "d", .constraint = &isSumEven },
    ac3.BinaryConstraint{ .name1 = "d", .name2 = "b", .constraint = &isSumEven },
    ac3.BinaryConstraint{ .name1 = "e", .name2 = "a", .constraint = &isLessThan },
};

With everything setup it is time to run the solver. solve will apply the AC-3 constraint solver and return true/false (where true means it is arc consistent, false means it is not). Once complete, the resulting variable domains can be viewed with a .domain() call. The example has before and after blocks to show the changes in variable domains. The one potentially unexpected part here is solve takes an allocator. Ideally I’d avoid it, but for now it is necessary for support of the internal work queue when doing binary constraint processing.

1
2
3
4
5
6
7
8
9
10
11
12
13
    std.debug.print("# Before\n", .{});
    for (variables) |v| {
        std.debug.print("{s} = {d}\n", .{ v.name, v.domain() });
    }

    const success = try ac3.solve(allocator, &variables, &unary_constraints, &binary_constraints);

    std.debug.print("# Success: {}\n", .{success});
    std.debug.print("# After\n", .{});
    for (variables) |v| {
        std.debug.print("{s} = {d}\n", .{ v.name, v.domain() });
    }
}

Running the above code shows that the definition of variables and constraints are arc consistent. “a” only includes even values; all of those values also are less than at least one value in “b”. Speaking of “b”, it only includes odd values. “c” only includes powers of two. “d” is only odd numbers, since the only way to add two values and get an even is if they are both even or both odd. But since “b” has to be odd, then all values of “d” must also be odd. Lastly, all values in “e” are less than at least one value in “a’. It looks like the domains were reducees as expected. Again, this doesn’t mean any combination is valid, but all of these values are potentially valid, if paired with the correct values from other variables. 

1
2
3
4
5
6
7
8
9
10
11
12
13
# Before
a = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 }
b = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 }
c = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 }
d = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 }
e = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 }
# Success: true
# After
a = { 2, 4, 6, 8, 10 }
b = { 1, 3, 5, 7, 9, 11 }
c = { 1, 2, 4, 8 }
d = { 1, 3, 5, 7, 9 }
e = { 1, 2, 3, 4, 5, 6, 7, 8, 9 }

What happens when a definition isn’t arc consistent? Below I add an additional constraint where a+b must be even. Based on what we just discovered, that’s impossible (a is always even, b is always odd; there is no combination where that could be even). The constraint solver determines this, as “a” is empty (“e” is too, since all its values must be less than “a”). The solver returns false, as it should.

1
BinaryConstraint{ .name1 = "a", .name2 = "b", .constraint = &isSumEven },
1
2
3
4
5
6
7
# Success: false
# After
a = {  }
b = { 1, 3, 5, 7, 9, 11 }
c = { 1, 2, 4, 8 }
d = { 1, 3, 5, 7, 9 }
e = {  }

This has been a brief revisiting of an AC-3 solver, but this time in Zig. Overall, this rewrite was a fun experience, and I even learned a couple things along the way. The ergonomics of Zig are decent. I do miss some of the ML niceities, but like with anything, its a series of trade offs. At least with constraint solving, I think the performance is worth it. Hopefully you found this useful. Until next time.

Related Posts: