Trying to solve Constraint over Ancestor Relation with SBV

Question

I'm trying to solve the following csp involing an ancestor relation in Haskell using the SBV Library (Version 7.12):

Give me the set of all persons who don't descend from Stephen.

My solution (see below) gets the following exception

*** Exception: SBV.Mergeable.List: No least-upper-bound for lists of differing size (1,0)

Question: Is it possible to solve constraints like this using SBV / using an SMT Solver and if - how do I need to formulate the problem?

My attempt at a solution:

{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveAnyClass      #-}

module Main where

import Data.SBV

data Person
  = Mary
  | Richard
  | Claudia
  | Christian
  | Stephen

mkSymbolicEnumeration ''Person

-- symbolic shorthands for person constructors
[mary, richard, claudia, christian, stephen] =
  map literal [Mary, Richard, Claudia, Christian, Stephen]

childOf :: [(Person, Person)]
childOf = [
    (Mary, Richard) ,
    (Richard, Christian),
    (Christian, Stephen)]

getAncestors :: Person -> [Person]
getAncestors p = go childOf p []
  where
    go [] _ acc = nub acc
    go ((p1, p2): rels) a acc
      | p1 == p = go rels p (p2:acc) ++ getAncestors p2
      | otherwise = go rels a acc

-- symbolic version of getAncestors
getSAncestors :: SBV Person -> [SBV Person]
getSAncestors p = ite (p .== mary) (map literal (getAncestors Mary))
                $ ite (p .== richard) (map literal (getAncestors Richard))
                $ ite (p .== claudia) (map literal (getAncestors Claudia))
                $ ite (p .== christian) (map literal (getAncestors Christian))
                                        (map literal (getAncestors Stephen))

cspAncestors :: IO AllSatResult
cspAncestors = allSat $ do
  (person :: SBV Person) <- free_
  constrain $ bnot $ stephen `sElem` (getSAncestors person)

Many thanks in advance!

Answer 1

The error message you get from SBV is truly cryptic, which doesn't really help, unfortunately. I've just pushed a patch to github, and the new error message is, I hope, a little better:

*** Exception:
*** Data.SBV.Mergeable: Cannot merge instances of lists.
*** While trying to do a symbolic if-then-else with incompatible branch results.
***
*** Branches produce different sizes: 1 vs 0
***
*** Hint: Use the 'SList' type (and Data.SBV.List routines) to model fully symbolic lists.

What SBV is trying to tell you is that when you have a symbolic if-then-else (as in your getSAncestor function) which returns a Haskell list of SBV Person's, then it cannot merge those branches unless each branch of the ite has exactly the same number of elements.

The problem

You might, of course, ask why there is such a restriction. Consider the following expression:

ite cond [s0, s1] [s2, s3, s4]

Intuitively, this should mean:

[ite cond s0 s2, ite cond s1 s3, ite cond ??? s4]

Unfortunately, there's nothing for SBV to substitute for the ???, and hence the error message. I hope that makes sense!

Two kinds of lists

SBV actually has two kinds of ways to represent a list of symbolic items. One is a good old Haskell list of symbolic values, as you were using; which is subject to the cardinality constraint I described above for each symbolic ite. The other is the fully symbolic list, that map to SMTLib sequences. Note that in both cases the size of the list is arbitrary but finite, but there's a difference in whether we treat the spine of the list symbolically or not.

Spine concrete symbolic lists

When you use a type like [SBV a], you are essentially saying "spine of this list is concrete, while the elements themselves are symbolic." This data type is most suitable when you know exactly how many elements you will have at each branch and they all have exactly the same size.

These lists map to a much simpler representation through the backend, essentially the "list" part is all handled in Haskell and elements are symbolically represented pointwise. This allows many SMT solvers to be used, even those that don't understand symbolic sequences. On the flip side, you cannot have a symbolic spine as you found out.

Spine symbolic lists

The second kind, as you can guess, is the kind of list that the spine itself is symbolic, and thus can support arbitrary ite conditions with no cardinality constraints. These map directly to SMTLib sequences, and are much more flexible. The down side is, not all SMT solvers support sequences, and the sequence logic is not decidable in general, so solvers might respond unknown, if it happens that the query falls outside of what their algorithms can handle. (Another down side is that sequence logic, as supported by z3 and cvc4, is rather immature, so solvers themselves might have bugs. But those are always reportable!)

The solution

To address your problem, you simply need to use SBV's spine symbolic lists, known as SList. The modifications needed for your example program are relatively simple:

{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

import Data.List

import Data.SBV.List as L

data Person
  = Mary
  | Richard
  | Claudia
  | Christian
  | Stephen

mkSymbolicEnumeration ''Person

-- symbolic shorthands for person constructors
[mary, richard, claudia, christian, stephen] =
  map literal [Mary, Richard, Claudia, Christian, Stephen]

childOf :: [(Person, Person)]
childOf = [
    (Mary, Richard) ,
    (Richard, Christian),
    (Christian, Stephen)]

getAncestors :: Person -> [Person]
getAncestors p = go childOf p []
  where
    go [] _ acc = nub acc
    go ((p1, p2): rels) a acc
      | p1 == p = go rels p (p2:acc) ++ getAncestors p2
      | otherwise = go rels a acc

-- symbolic version of getAncestors
getSAncestors :: SBV Person -> SList Person
getSAncestors p = ite (p .== mary)      (literal (getAncestors Mary))
                $ ite (p .== richard)   (literal (getAncestors Richard))
                $ ite (p .== claudia)   (literal (getAncestors Claudia))
                $ ite (p .== christian) (literal (getAncestors Christian))
                                        (literal (getAncestors Stephen))

cspAncestors :: IO AllSatResult
cspAncestors = allSat $ do
  (person :: SBV Person) <- free "person"
  constrain $ sNot $ L.singleton stephen `L.isInfixOf` (getSAncestors person)

(Note: I had to change bnot to sNot since I'm using SBV 8.0 available from hackage; which had that name change. If you're using 7.12, you should keep the bnot. Also note the use of SList Person as opposed to [SBV Person], which tells SBV to use spine symbolic lists.)

When I run this, I get:

*Main> cspAncestors
Solution #1:
  person = Claudia :: Person
Solution #2:
  person = Stephen :: Person
Found 2 different solutions.

I haven't really checked whether the answer is correct, but I trust it should be! (If not, please report.)

I hope that gives an overview of the problem and how to address it. While an SMT solver cannot beat a custom CSP solver, I think it can be a great alternative when you don't have a dedicated algorithm. Hopefully Haskell/SBV makes it easier to use!