haskell - 约束 SBV 中某种类型元素计数的符号列表

Question

使用 SBV 库，我试图满足状态符号列表上的条件:

data State = Intro | Start | Content | Comma | Dot
mkSymbolicEnumeration ''State

-- examples of such lists
[Intro, Start, Content, Comma, Start, Comma, Content, Dot]
[Intro, Comma, Start, Content, Comma, Content, Start, Dot]

除了我需要最终列表完全包含 n 之外，一切正常任一 [Intro, Start, Content] 的元素总共。目前我使用有界过滤器来做到这一点:

answer :: Int -> Symbolic [State]
answer n = do
    seq <- sList "seq"

    let maxl = n+6
    let minl = n+2
    constrain $ L.length seq .<= fromIntegral maxl
    constrain $ L.length seq .>= fromIntegral minl

    -- some additional constraints hidden for brevity purposes

    let etypes e = e `sElem` [sIntro, sStart, sContent]
    constrain $ L.length (L.bfilter maxl etypes seq) .== fromIntegral n

如您所见，列表可以是 n+2 之间的任意长度。和 n+6 ，重要的一点是它的计数是正确的 [sIntro, sStart, sContent]其中的元素。
一切正常，除了 极减缓。喜欢，对于 n=4这需要几秒钟，但对于 n>=6它需要永远(超过 30 分钟并且仍在计数)。如果我删除有界过滤器约束，结果是即时的 n最多 25 个左右。
最后，我不是特别关心使用 L.bfilter .我所需要的只是一种声明最终符号列表应包含 的方法。正好 n某些给定类型的元素。
-> 有没有更快的方法可以满足 count(sIntro || sStart || sContent) ?
- 在评论中讨论后编辑:
下面的代码应该确保所有有效元素都在 elts 中。列表。例如，如果我们数 8 valids来自 elts 的元素，那么我们 take 8 elts我们计算 validTaken此子列表中的有效元素。如果结果是 8 ，这意味着所有的 8 valids元素位于 elts 中.可悲的是，这导致了一个系统的 Unsat结果，即使在删除所有其他约束之后。不过，当针对一些虚拟元素列表进行测试时，该函数运行良好。

-- | test that all valid elements are upfront in the list of elements
validUpFront :: SInteger -> [Elem] -> SBool
validUpFront valids elts =
    let takeValids = flip take elts <$> (fromInteger <$> unliteral valids)
        validTaken = sum $ map (oneIf . included) $ fromMaybe [] takeValids
    in valids .== validTaken

-- ...

answer n = runSMT $ do

    -- ...

    let valids = sum $ map (oneIf . included) elts :: SInteger
    constrain $ validUpFront valids elts

Answer 1

序列逻辑的求解器虽然用途广泛，但速度却是出了名的慢。对于这个特定问题，我建议使用常规的 bool 逻辑，这样会表现得更好。以下是我对您的问题进行编码的方式:

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

import Data.SBV
import Data.SBV.Control
import Data.Maybe
import Control.Monad

data State = Intro | Start | Content | Comma | Dot
mkSymbolicEnumeration ''State

data Elem = Elem { included :: SBool
                 , element  :: SState
                 }

new :: Symbolic Elem
new = do i <- free_
         e <- free_
         pure Elem {included = i, element = e}

get :: Elem -> Query (Maybe State)
get e = do isIn <- getValue (included e)
           if isIn
               then Just <$> getValue (element e)
               else pure Nothing

answer :: Int -> IO [State]
answer n = runSMT $ do
    let maxl = n+6
    let minl = n+2

    -- allocate upto maxl elements
    elts <- replicateM maxl new

    -- ask for at least minl of them to be valid
    let valids :: SInteger
        valids = sum $ map (oneIf . included) elts
    constrain $ valids .>= fromIntegral minl

    -- count the interesting ones
    let isEtype e  = included e .&& element e `sElem` [sIntro, sStart, sContent]
        eTypeCount :: SInteger
        eTypeCount = sum $ map (oneIf . isEtype) elts

    constrain $ eTypeCount .== fromIntegral n

    query $ do cs <- checkSat
               case cs of
                 Sat -> catMaybes <$> mapM get elts
                 _   -> error $ "Query is " ++ show cs

示例运行:

*Main> answer 5
[Intro,Comma,Comma,Intro,Intro,Intro,Start]

我已经能够跑到 answer 500在我相对较旧的机器上大约 5 秒后返回。
确保所有有效值都在开头
使所有有效元素都位于列表开头的最简单方法是计算包含值中的交替数，并确保只允许一个这样的转换:

-- make sure there's at most one-flip in the sequence.
-- This'll ensure all the selected elements are up-front.
let atMostOneFlip []     = sTrue
    atMostOneFlip (x:xs) = ite x (atMostOneFlip xs) (sAll sNot xs)

constrain $ atMostOneFlip (map included elts)

这将确保所有有效值都位于包含无效条目的列表的后缀之前。当您编写其他属性时，您必须检查当前元素和下一个元素是否有效。以模板形式:

foo (x:y:rest) = ((included x .&& included y) .=> (element y .== sStart .=> element x .== sDot))
                .&& foo (y:rest)

通过象征性地查看 included x 的值和 included y ，您可以确定它们是否都包含在内，或者是否包含 x是最后一个元素，或者如果它们都出来了；并在每种情况下写出相应的约束作为含义。上面显示了当您处于序列中间某处时的情况，同时带有 x和 y包括。