Satchmo.Counting.Direct

functions in this module have no extra variables but exponential cost.

Documentation

atleast :: MonadSAT m => Int -> [Boolean] -> m Boolean

atmost :: MonadSAT m => Int -> [Boolean] -> m Boolean

exactly :: MonadSAT m => Int -> [Boolean] -> m Boolean

assert_implies_atmost :: MonadSAT m => [Boolean] -> Int -> [Boolean] -> m ()

(and ys) implies (atmost k xs)

assert_implies_exactly :: MonadSAT m => [Boolean] -> Int -> [Boolean] -> m ()

asserting that (and ys) implies (exactly k xs)