partition.hs

import Data.SBV
import Data.List (partition)

sumSplit :: [Integer] -> IO (Maybe (Integer, [Integer], [Integer]))
sumSplit xs = do r <- satWith z3 $ do zs <- mkFreeVars (length xs)
                                      let sums sofar []            = sofar
                                          sums (i,o) ((f, v):rest) = sums (ite f (i+v, o) (i, o+v)) rest
                                          (f, s) = sums (0, 0) $ zip zs (map literal xs)
                                      return $ f .== s
                 case getModel r of
                   Left _        -> return Nothing
                   Right (_, bs) -> let (f, s) = partition fst $ zip bs xs
                                        part1  = map snd f
                                        part2  = map snd s
                                    in return $ Just (sum part1, part1, part2)

-- Example calls in ghci:
-- *Main> sumSplit []
-- Just (0,[],[])
-- *Main> sumSplit [0]
-- Just (0,[],[0])
-- *Main> sumSplit [1]
-- Nothing
-- *Main> sumSplit [1,3,5,1,3,-1,2,0]
-- Just (7,[3,3,-1,2],[1,5,1,0])
-- *Main> sumSplit [1,3,5,1,3,-1,2,0,12]
-- Just (13,[-1,2,12],[1,3,5,1,3,0])