haskell - 尝试用SBV解决祖先关系的约束

Question

我正在尝试使用SBV Library解决Haskell中涉及祖先关系的以下csp (7.12 版):

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

我的解决方案(见下文)出现以下异常

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

问题:是否可以使用 SBV/使用 SMT 求解器来解决这样的约束，如果 - 我需要如何制定问题？

我尝试的解决方案:

{-# 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 函数中)时，它会返回 Haskell 列表 SBV Person 的，那么它无法合并这些分支，除非 ite 的每个分支具有完全相同的元素数量。

问题

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

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

直观上，这应该意味着:

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

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

两种列表

SBV实际上有两种方式来表示符号项列表。一个是一个很好的旧 Haskell 符号值列表，正如您所使用的；它受到我上面为每个符号项目描述的基数约束。另一个是完全符号列表，映射到 SMTLib 序列。请注意，在这两种情况下，列表的大小都是任意但有限的，但是我们是否以符号方式处理列表的主干是有区别的。

Spine 具体符号列表

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

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

Spine 符号列表

正如您所猜到的，第二种列表的主干本身是符号性的，因此可以支持任意的ite条件而没有基数限制。这些直接映射到 SMTLib 序列，并且更加灵活。缺点是，并非所有 SMT 求解器都支持序列，并且序列逻辑通常不可判定，因此如果查询超出其算法可以处理的范围，求解器可能会响应未知。 (另一个缺点是 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 提供的 SB​​V 8.0；该名称已更改。如果您使用的是 7.12 ，您应该保留 bnot。另请注意 SList Person 的使用，而不是 [SBV Person]，它告诉 SBV 使用 spin 符号列表。)

当我运行这个时，我得到:

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

我还没有真正检查过答案是否正确，但我相信应该是正确的! (如果没有，请报告。)

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