试图用 SBV 解决祖先关系的约束

Question

我正在尝试使用 SBV Library（版本 7.12）解决以下涉及 Haskell 中祖先关系的 csp：

给我所有不是斯蒂芬后裔的人的集合。

我的解决方案（见下文）得到以下异常

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

问题：是否可以使用 SBV / 使用 SMT Solver 解决此类约束，如果 - 我需要如何制定问题？

我的解决方案尝试：

{-# 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)

非常感谢！

Answer 1

您从 SBV 收到的错误消息确实很神秘，很遗憾，这并没有真正的帮助。我刚刚向 github 推送了一个补丁，我希望新的错误信息会好一点：

*** 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.

SBV 试图告诉您的是，当您有一个符号 if-then-else（如在您的 getSAncestor 函数中）返回 SBV Person 的 Haskell 列表时，那么它不能合并这些分支，除非ite 的每个分支具有完全相同数量的元素。

问题

当然，您可能会问为什么会有这样的限制。考虑以下表达式：

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

直观地说，这应该意味着：

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

不幸的是，SBV 没有任何东西可以替代???，因此出现了错误消息。我希望这是有道理的！

两种列表

SBV 实际上有两种方式来表示符号项列表。一个是一个很好的旧 Haskell list 符号值，就像您使用的那样；这受我上面描述的每个符号项的基数约束。另一个是完全符号列表，映射到 SMTLib 序列。请注意，在这两种情况下，列表的大小都是任意的，但也是有限的，但是我们是否象征性地对待列表的脊椎是不同的。

Spine 具体符号列表

当你使用像[SBV a] 这样的类型时，你实际上是在说“这个列表的主干是具体的，而元素本身是象征性的”。当您确切知道每个分支将有多少个元素并且它们都具有完全相同的大小时，此数据类型最合适。

这些列表通过后端映射到一个更简单的表示形式，本质上“列表”部分全部在 Haskell 中处理，元素以符号方式逐点表示。这允许使用许多 SMT 求解器，即使是那些不理解符号序列的求解器。另一方面，你不能像你发现的那样有一个象征性的脊椎。

脊柱符号列表

第二类，你可以猜到，是一种spine本身是符号的列表，因此可以支持任意ite条件而没有基数约束。这些直接映射到 SMTLib 序列，并且更加灵活。不利的一面是，并非所有 SMT 求解器都支持序列，并且序列逻辑通常不可确定，因此如果查询超出其算法可以处理的范围，求解器可能会回复 unknown。 （另一个缺点是 z3 和 cvc4 支持的序列逻辑相当不成熟，因此求解器本身可能存在错误。但这些总是可以报告的！）

解决办法

要解决您的问题，您只需使用 SBV 的脊椎符号列表，称为 SList。您的示例程序所需的修改相对简单：

{-# 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)

（注意：我必须将bnot 更改为sNot，因为我使用的是hackage 提供的SBV 8.0；它的名称已更改。如果您使用的是7.12，则应保留bnot。另外注意使用SList Person 而不是[SBV Person]，后者告诉SBV 使用spine 符号列表。）

当我运行它时，我得到：

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

我还没有真正检查过答案是否正确，但我相信应该是的！ （如果不是，请报告。）

我希望能够概述问题以及如何解决它。虽然 SMT 求解器无法击败自定义 CSP 求解器，但我认为当您没有专用算法时，它可能是一个很好的选择。希望 Haskell/SBV 让它更易于使用！