限制 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]

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

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。我所需要的只是一种声明最终符号列表应该包含 exactly n 某些给定类型的元素的方法。

-> 有没有更快的方法可以满足count(sIntro || sStart || sContent)?

-- 在评论中讨论后编辑：

下面的代码应该确保所有有效元素都在 elts 列表的前面。例如，如果我们从 elts 中计算 8 valids 个元素，那么我们 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

序列逻辑的求解器虽然用途广泛，但速度非常慢。对于这个特殊问题，我建议使用常规布尔逻辑，这样性能会好得多。以下是我对您的问题进行编码的方式：

{-# 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。

限制 SBV 中特定类型元素计数的符号列表

Constrain a symbolic list on count of elements of a certain type in SBV

haskell

smt

sbv

确保所有有效值都在开头