3

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

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

我的解决方案（见下文）出现以下异常

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

提前谢谢了！

4

1 回答 1

3

您从 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 试图告诉您的是，当您有一个返回Haskell列表的符号 if-then-else（如在您的getSAncestor函数中）时，除非每个分支具有完全相同的编号，否则它无法合并这些分支的元素。SBV Personite

问题

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

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

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

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

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

两种列表

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

脊柱混凝土符号表

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

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

脊柱符号列表

第二种，你可以猜到，是一种脊本身是符号的列表，因此可以支持任意 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为，因为我使用的是sNothackage 提供的 SB​​V 8.0；该名称已更改。如果您使用的是 7.12，则应保留使用脊椎符号列表。）bnotSList Person[SBV Person]

当我运行它时，我得到：

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

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

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

于 2019-01-26T00:25:41.227 回答