🕵️‍♂️ Holmes

Holmes is a library for computing constraint-solving problems. Under the hood, it uses propagator networks and conflict-directed clause learning to optimise the search over the parameter space.

Now available on Hackage!

👟 Example

Dinesman's problem is a nice first example of a constraint problem. In this problem, we imagine five people — Baker, Cooper, Fletcher, Miller, and Smith — living in a five-story apartment block, and we must figure out the floor on which each person lives. Here's how we state the problem with Holmes:

import Data.Holmes

dinesman :: IO (Maybe [ Defined Int ])
dinesman = do
  let guesses = 5 `from` [1 .. 5]

  guesses `satisfying` \[ baker, cooper, fletcher, miller, smith ] -> and'
    [ distinct [ baker, cooper, fletcher, miller, smith ]
    , baker ./= 5
    , cooper ./= 1
    , fletcher ./= 1 .&& fletcher ./= 5
    , miller .> cooper
    , abs' (smith .- fletcher) ./= 1
    , abs' (fletcher .- cooper) ./= 1
    ]

👣 Step-by-step problem-solving

Now we've written the poster example, how do we go about stating and solving our own constraint problems?

⚖️ 0. Pick a parameter type

Right now, there are two parameter type constructors: Defined and Intersect. The choice of type determines the strategy by which we solve the problem:

Defined only permits two levels of knowledge about a value: nothing and everything. In other words, it doesn't support a notion of partial information; we either know a value, or we don't. This is fine for small problem spaces, particularly when few branches are likely to fail, but we can usually achieve faster results using another type.
Intersect stores a set of "possible answers", and attempts to eliminate possibilities as the computation progresses. For problems with many constraints, this will produce significantly faster results than Defined as we can hopefully discover failures much earlier.

It would seem that Intersect would be the best choice in most cases, but beware: it will only work for small enum types. An Intersect Int for which we have no knowledge will contain every possible Int, and will therefore take an intractable time to compute. Defined has no such restrictions.

🗺 1. State the parameter space

Next, we need to produce a Config stating the search space we want to explore when looking for satisfactory inputs. The simplest way to do this is with the from function:

from :: Int -> [ x ] -> Config Holmes (Defined x)

from :: Int -> [ x ] -> Config Holmes (Intersect x)

If, for example, we wanted to solve a Sudoku problem, we might say something like this:

definedConfig :: Config Holmes (Defined Int)
definedConfig = 81 `from` [ 1 .. 9 ]

We read this as, "81 variables whose values must all be numbers between 1 and 9". At this point, we place no constraints (such as uniqueness of rows or columns); we're just stating the possible range of values that could exist in each parameter.

We could do the same for Intersect, but we'd first need to produce some enum type to represent our parameter space:

data Value = V1 | V2 | V3 | V4 | V5 | V6 | V7 | V8 | V9
  deriving stock (Eq, Ord, Show, Enum, Bounded, Generic)
  deriving anyclass (Hashable)

instance Num Value where -- Syntactic sugar for numeric literals.
  fromInteger = toEnum . pred . fromInteger

Now, we can produce an Intersect parameter space. Because we can now work with a type who has only 9 values, rather than all possible Int values, producing the initial possibilities list becomes tractable:

intersectConfig :: Config Holmes (Intersect Value)
intersectConfig = 81 `from` [ 1 .. 9 ]

There's one more function that lets us do slightly better with an Intersect strategy, and that's using:

using :: [ Intersect Value ] -> Config Holmes (Intersect Value)

With using, we can give a precise "initial state" for all the Intersect variables in our system. This, it turns out, is very convenient when we're trying to state sudoku problems:

squares :: Config Holmes (Intersect Value)
squares = let x = mempty in using
    [ x, 5, 6,   x, x, 3,   x, x, x
    , 8, 1, x,   x, x, x,   x, x, x
    , x, x, x,   5, 4, x,   x, x, x

    , x, x, 4,   x, x, x,   x, 8, 2
    , 6, x, 8,   2, x, 4,   3, x, 7
    , 7, 2, x,   x, x, x,   4, x, x

    , x, x, x,   x, 7, 8,   x, x, x
    , x, x, x,   x, x, x,   x, 9, 3
    , x, x, x,   3, x, x,   8, 2, x
    ]

Now, let's write some constraints!

📯 2. Declare your constraints

Typically, your constraints should be stated as a predicate on the input parameters, with a type that, when specialised to your problem, should look something like [Prop Holmes (Defined Int)] -> Prop Holmes (Defined Bool). Now, what's this Prop type?

🕸 Propagators

If this library has done its job properly, this predicate shouldn't look too dissimilar to regular predicates. However, behind the scenes, the Prop type is wiring up a lot of relationships.

As an example, consider the (+) function. This has two inputs and one output, and the output is the sum of the two inputs. This is totally fixed, and there's nothing we can do about it. This is fine when we write normal programs, because we only have one-way information flow: input flows to output, and it's as simple as that.

When we come to constraint problems, however, we have multi-way information flow: we might know the output before we know the inputs! Ideally, it'd be nice in these situations if we could "work backwards" to the information we're missing.

When we say x .+ y .== z, we actually wire up multiple relationships: x + y = z, z - y = x, and z - x = y. That way, as soon as we learn two of the three values involved in addition, we can infer the other!

The operators provided by this library aim to maximise information flow around a propagator network by automatically wiring up all the different identities for all the different operators. We'll see later that this allows us to write seemingly-magical functions like backwards: given a function and an output, we can produce the function's input!

🛠 The problem-solving toolkit

With all this in mind, the following functions are available to us for multi-directional information flow. We'll leave the type signatures to Haddock, and instead just run through the functions and either their analogous regular functions or a brief explanation of what they do:

🎚 Boolean functions

| Function | Analogous function / notes | | --:|:-- | | (.&&) | (&&) | | all' | all | | allWithIndex' | all', but the predicate also receives the list index | | and' | and | | (.\|\|) | (\|\|) | | any' | any | | anyWithIndex' | any', but the predicate also receives the list index | | or' | or | | not' | not | | false | False | | true | True |

🏳️‍🌈 Equality functions

| Function | Analogous function / notes | | --:|:-- | | (.==) | (==) | | (./=) | (/=) | | distinct | Are all list elements different (according to (./=))? |

🥈 Comparison functions

| Function | Analogous function / notes | | --:|:-- | | (.<) | (<) | | (.<=) | (<=) | | (.>) | (>) | | (.>=) | (>=) |

🎓 Arithmetic functions

| Function | Analogous function / notes | | --:|:-- | | (.*) | (*) | | (./) | (/) | | (.+) | (+) | | (.-) | (-) | | (.%.) | mod | | (.*.) | (*) for integral functions | | (./.) | div | | abs' | abs | | negate' | negate | | recip' | recip |

🌱 Information-generating functions

The analogy gets stretched a bit here, unfortunately. It's perhaps helpful to think of these functions in terms of Intersect:

(.$) maps over the remaining candidates in an Intersect.
zipWith' creates an Intersect of the cartesian product of the two given Intersects, with the pairs applied to the given function.
(.>>=) takes every remaining candidate, applies the given function, then unions the results to produce an Intersect of all possible results.

Using the above toolkit, we could express the constraints of our sudoku example. After we establish some less interesting functions for splitting up our 81 inputs into helpful chunks...

rows :: [ x ] -> [[ x ]]
rows [] = []
rows xs = take 9 xs : rows (drop 9 xs)

columns :: [ x ] -> [[ x ]]
columns = transpose . rows

subsquares :: [ x ] -> [[ x ]]
subsquares xs = do
  x <- [ 0 .. 2 ]
  y <- [ 0 .. 2 ]

  let subrows = take 3 (drop (y * 3) (rows xs))
      values  = foldMap (take 3 . drop (x * 3)) subrows

  pure values

... we can use the propagator toolkit to specify our constraints in a delightfully straightforward way:

constraints :: forall m. MonadCell m => [ Prop m (Intersect Value) ] -> Prop m (Intersect Bool)
constraints board = and'
  [ all' distinct (columns    board)
  , all' distinct (rows       board)
  , all' distinct (subsquares board)
  ]

_

Holmes

Install / Use

README