2

使用 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列表的前面。例如，如果我们valids从 中计算 8 个元素elts，那么我们take 8 elts将计算validTaken此子列表中的有效元素。如果结果是8，则意味着所有 8valids个元素都在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
4

1 回答 1

2

序列逻辑的求解器虽然用途广泛，但速度却是出了名的慢。对于这个特殊的问题，我建议使用常规的布尔逻辑，它会执行得更好。这是我对您的问题进行编码的方式：

{-# 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 秒内运行 up to which 返回。

确保所有有效值都在开头

使所有有效元素都位于列表开头的最简单方法是计算包含值中的交替，并确保只允许一个这样的转换：

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

通过象征性地查看 and 的值included x，included y您可以确定它们是否都包含在内，或者是否x是最后一个元素，或者它们是否都在外面；并将相应的约束写为每种情况下的含义。上面显示了当你在某个地方的序列中间时的情况，两者都x包括y在内。

于 2020-10-26T18:27:30.570 回答