haskellsmtsbv

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


Using the SBV library, I'm trying to satisfy conditions on a symbolic list of states:

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]

All works fine except that I need the final list to contain exactly n elements of either [Intro, Start, Content] in total. Currently I do it using a bounded filter:

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

As you can see, the list can be of any length between n+2 and n+6, the important bit is that it has the right count of [sIntro, sStart, sContent] elements within it.

It works all fine, except it's extremely slow. Like, for n=4 it takes a few seconds, but for n>=6 it takes forever (more than 30 minutes and still counting). If I remove the bounded filter constraint, the result is instant with n up to 25 or so.

In the end, I don't particularly care about using L.bfilter. All I need is a way to declare that the final symbolic list should contain exactly n elements of some given types.

-> Is there a faster way to be able to satisfy for count(sIntro || sStart || sContent)?

-- EDIT after discussion in comments:

The code below is supposed to make sure that all valid elements are up-front in the elts list. For example, if we count 8 valids elements from elts, then we take 8 elts and we count the validTaken valid elements in this sub-list. If the result is 8, it means that all the 8 valids elements are up-front in elts. Sadly, this results in a systematic Unsat outcome, even after removing all other constraints. The function works well when tested against some dummy lists of elements, though.

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

Solution

  • Solvers for the sequence logic, while quite versatile, are notoriously slow. For this particular problem, I'd recommend using regular boolean logic, which will perform much better. Here's how I'd code your problem:

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

    Example run:

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

    I've been able to run upto answer 500 which returned in about 5 seconds on my relatively old machine.

    Making sure all valids are at the beginning

    The easiest way to make all the valid elements are at the beginning of the list is to count the alternations in the included value, and make sure you allow only one such transition:

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

    This'll make sure all the valids precede the suffix of the list that contain the invalid entries. When you write your other properties, you'd have to check that both the current element and the next element is valid. In template form:

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

    By symbolically looking at the values of included x and included y, you can determine if they are both included, or if x is the last element, or if they're both out; and write the corresponding constraints as implications in each case. The above shows the case for when you're in the middle of the sequence somewhere, with both x and y included.