如何解决将符号列表约束为SBV中某种类型的元素数
使用SBV库,我试图满足符号状态列表中的条件:
data State = Intro | Start | Content | Comma | Dot
mkSymbolicEnumeration ''State
-- examples of such lists
[Intro,Start,Content,Comma,Dot]
[Intro,Dot]
一切正常,除了我需要最终列表完全包含n
中的[Intro,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,sContent]
个元素的数量正确。
除了非常慢缓慢之外,一切正常。就像,n=4
会花费几秒钟,而n>=6
会花费永久(超过30分钟,并且还在计算)。如果我删除了有界过滤器约束,则结果是n
即时达到25左右。
最后,我并不特别在意使用L.bfilter
。我需要的是一种声明最终符号列表应包含某些特定类型的恰好 n
元素的方法。
-> 是否有更快的方法可以满足count(sIntro || sstart || sContent)
?
-评论讨论后进行编辑:
下面的代码应确保所有有效元素在elts
列表中位于最前面。例如,如果我们从valids
计算8个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
解决方法
序列逻辑的求解器虽然用途广泛,但众所周知它速度很慢。对于此特定问题,我建议使用常规布尔逻辑,它将表现得更好。这是我如何编码您的问题:
{-# 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,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
的情况。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。