ClpMatrix

Made for my own edification. Exploring the question of translating constraint propagation to matrix convolution.

The mapping

A CLP(FD) engine holds two kinds of state:

• a domain per variable -- the set of values it could still take;
• a set of constraints -- relations that prune domains when a value loses all support in some neighboring domain.

It propagates by repeatedly asking, for each constraint, "does every remaining value on each side still have a compatible partner on the other side?", removing the ones that don't, until nothing changes (a fixpoint). That's arc consistency, normally implemented with a worklist/queue of (variable, constraint) pairs to revisit.

Every piece of that has a direct matrix form:

CLP(FD) concept	Matrix form
domain of variable x (size n)	a {n} 0/1 vector -- 1 if the value at that index is still possible
binary constraint between x and y	an {n, m} 0/1 compatibility matrix M, where M[i][j] = 1 iff value i of x is compatible with value j of y
"does value j of y still have support in x?"	(domain_x · M)[j] > 0 -- an ordinary vector-matrix product, thresholded at zero
pruning y's domain	domain_y = domain_y AND (domain_x · M > 0)
one round of propagation	do that for every constraint, both directions (M for x -> y, Mᵀ for y -> x)
fixpoint	repeat rounds until no domain changes

Domains are 0/1, so "is there at least one supporting value" is exactly "is this dot product greater than zero" -- no boolean-specific machinery needed, ordinary real-valued matrix multiplication does the job. ClpMatrix.Compiler builds the vectors and matrices from a problem declaration; ClpMatrix.Propagator runs the loop above to a fixpoint. That loop still walks the constraint list once per round -- it's matrix arithmetic, but it's also still "walking the graph" edge by edge.

Usage

defmodule MyProblem do
  use ClpMatrix.Problem

  domain :x, 1..10
  domain :y, 1..10

  constraint :x, :y, fn x, y -> y == x + 3 end
end

ClpMatrix.solve(MyProblem) |> ClpMatrix.pretty_print()

mix deps.get
mix test
mix run examples/chained_arithmetic.exs     # general case: edge-loop propagation
mix run examples/convolutional_chain.exs    # edge-loop vs. conv, cross-checked

Layout

• lib/clp_matrix/problem.ex -- the domain/constraint DSL for declaring a problem.
• lib/clp_matrix/compiler.ex -- turns a declared problem into domain vectors and compatibility matrices.
• lib/clp_matrix/propagator.ex -- the general fixpoint loop over the constraint list.
• lib/clp_matrix.ex -- solve/2 and pretty_print/1.
• examples/ -- the general case, and the convolution equivalence.

Known limitations (i.e. why this isn't a CSP solver)

• Binary constraints only. No native support for constraints over 3+ variables (e.g. x + y = z) or global constraints (e.g. all_different). Both would need a different matrix representation (tensors of rank > 2, or a different pruning rule entirely).

• Propagation only, no search. Arc consistency prunes domains but doesn't always find a single solution -- e.g. binary != constraints alone can't detect that three mutually-adjacent variables can't all take 2 of 3 shared values (that needs all_different's global view, or backtracking search on top of propagation). Domains that come out of ClpMatrix.solve/2 may still have more than one value in them; that's expected, not a bug.

• Only for small domains This becomes very slow for large integer fields. There are various optimisations for this, but for ZK purposes for example it's unnecessary, as you can just take a trace and verify that.