Попытка решить Ограничение Отношения Предка с SBV

Question

Я пытаюсь решить следующую csp, включающую отношение предка в Haskell, используя библиотеку SBV (версия 7.12):

Дайте мне набор всех людей, которые не происходят от Стивена.

Мое решение (см. Ниже) получает следующее исключение

*** 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 функция), которая возвращает список Haskell SBV Persons, то он не может объединить эти ветви, если каждая ветвь ite имеет точно такое же количество элементов.

Эта проблема

Вы можете, конечно, спросить, почему существует такое ограничение. Рассмотрим следующее выражение:

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, даже те, которые не понимают символьные последовательности. С другой стороны, вы не можете иметь символический позвоночник, как вы узнали.

Списки символов позвоночника

Второй тип, как вы можете догадаться, это вид списка, в котором сам позвоночник является символическим и, следовательно, может поддерживать произвольные условия ите без ограничений на количество элементов. Они отображаются непосредственно на последовательности 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 так как я использую SBV 8.0, доступный от hackage; который изменил это имя. Если вы используете 7.12, вы должны сохранить bnot, Также обратите внимание на использование SList Person в отличие от [SBV Person], который говорит SBV использовать символические списки позвоночника.)

Когда я запускаю это, я получаю:

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

Я действительно не проверил, является ли ответ правильным, но я верю, что так и должно быть! (Если нет, пожалуйста, сообщите.)

Я надеюсь, что это дает обзор проблемы и как ее решить. Хотя SMT-решатель не может превзойти собственный CSP-решатель, я думаю, что он может быть отличной альтернативой, если у вас нет выделенного алгоритма. Надеюсь, Haskell/SBV облегчает использование!