subset_sum.hs

#!/usr/bin/env stack
-- stack --install-ghc runghc --package sbv

import Data.Foldable
import Data.SBV

-- Encoding the Subset sum problem
-- https://en.wikipedia.org/wiki/Subset_sum_problem
subsetSum :: [SInt64] -> SInt64 -> Int -> IO SatResult
subsetSum set target subsetLength = sat $ do
  sxs <- mkExistVars subsetLength
  constrain $ bAll (`sElem` set) sxs
  constrain $ allDifferent sxs
  return $ sum sxs .== target

{-
Should output:

  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 3 :: Int64
  Unsatisfiable
  Satisfiable. Model:
    s0 = 25 :: Int64
  Satisfiable. Model:
    s0 = 23 :: Int64
    s1 = 2 :: Int64
  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 10 :: Int64
    s2 = 13 :: Int64
  Satisfiable. Model:
    s0 = 8 :: Int64
    s1 = 9 :: Int64
    s2 = 5 :: Int64
    s3 = 3 :: Int64
  Satisfiable. Model:
    s0 = 10 :: Int64
    s1 = 2 :: Int64
    s2 = 6 :: Int64
    s3 = 3 :: Int64
    s4 = 4 :: Int64
  Satisfiable. Model:
    s0 = 10 :: Int64
    s1 = 2 :: Int64
    s2 = 5 :: Int64
    s3 = 3 :: Int64
    s4 = 4 :: Int64
    s5 = 1 :: Int64
  Unsatisfiable
  Unsatisfiable
  Unsatisfiable
  Unsatisfiable
  Satisfiable. Model:
    s0 = 42 :: Int64
  Satisfiable. Model:
    s0 = 14 :: Int64
    s1 = 28 :: Int64
  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 10 :: Int64
    s2 = 30 :: Int64
  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 12 :: Int64
    s2 = 5 :: Int64
    s3 = 23 :: Int64
  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 19 :: Int64
    s2 = 7 :: Int64
    s3 = 1 :: Int64
    s4 = 13 :: Int64
  Satisfiable. Model:
    s0 = 5 :: Int64
    s1 = 9 :: Int64
    s2 = 8 :: Int64
    s3 = 1 :: Int64
    s4 = 13 :: Int64
    s5 = 6 :: Int64
  Satisfiable. Model:
    s0 = 4 :: Int64
    s1 = 1 :: Int64
    s2 = 5 :: Int64
    s3 = 13 :: Int64
    s4 = 2 :: Int64
    s5 = 14 :: Int64
    s6 = 3 :: Int64
  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 3 :: Int64
    s2 = 1 :: Int64
    s3 = 4 :: Int64
    s4 = 7 :: Int64
    s5 = 9 :: Int64
    s6 = 6 :: Int64
    s7 = 10 :: Int64
  Unsatisfiable
  Unsatisfiable
  Satisfiable. Model:
    s0 = 81 :: Int64
  Satisfiable. Model:
    s0 = 69 :: Int64
    s1 = 12 :: Int64
  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 10 :: Int64
    s2 = 69 :: Int64
  Satisfiable. Model:
    s0 = 12 :: Int64
    s1 = 26 :: Int64
    s2 = 42 :: Int64
    s3 = 1 :: Int64
  Satisfiable. Model:
    s0 = 18 :: Int64
    s1 = 1 :: Int64
    s2 = 38 :: Int64
    s3 = 22 :: Int64
    s4 = 2 :: Int64
  Satisfiable. Model:
    s0 = 2 :: Int64
    s1 = 4 :: Int64
    s2 = 12 :: Int64
    s3 = 3 :: Int64
    s4 = 44 :: Int64
    s5 = 16 :: Int64
  Satisfiable. Model:
    s0 = 13 :: Int64
    s1 = 1 :: Int64
    s2 = 19 :: Int64
    s3 = 17 :: Int64
    s4 = 12 :: Int64
    s5 = 16 :: Int64
    s6 = 3 :: Int64
  Satisfiable. Model:
    s0 = 50 :: Int64
    s1 = 7 :: Int64
    s2 = 4 :: Int64
    s3 = 3 :: Int64
    s4 = 2 :: Int64
    s5 = 6 :: Int64
    s6 = 1 :: Int64
    s7 = 8 :: Int64
  Satisfiable. Model:
    s0 = 9 :: Int64
    s1 = 8 :: Int64
    s2 = 1 :: Int64
    s3 = 18 :: Int64
    s4 = 12 :: Int64
    s5 = 4 :: Int64
    s6 = 14 :: Int64
    s7 = 2 :: Int64
    s8 = 13 :: Int64
  Satisfiable. Model:
    s0 = 7 :: Int64
    s1 = 5 :: Int64
    s2 = 2 :: Int64
    s3 = 4 :: Int64
    s4 = 17 :: Int64
    s5 = 6 :: Int64
    s6 = 1 :: Int64
    s7 = 12 :: Int64
    s8 = 18 :: Int64
    s9 = 9 :: Int64
-}

main :: IO ()
main = do
   print =<< subsetSum [1, 2, 3] 5 2
   print =<< subsetSum [1..10] 5 3
   traverse_ (\len -> print =<< subsetSum [1..100] 25 len) [1..10]
   traverse_ (\len -> print =<< subsetSum [1..100] 42 len) [1..10]
   traverse_ (\len -> print =<< subsetSum [1..100] 81 len) [1..10]