Search code examples
haskellsmtsatisfiability

How to run SAT calls in parallel using the picosat haskell bindings?

import Picosat
import Control.Applicative

main :: IO ()
main = do
  dimacsList1 <- (read <$> getLine) :: IO [[Integer]]
  dimacsList2 <- (read <$> getLine) :: IO [[Integer]]

  res1 <- solve dimacsList1
  res2 <- solve dimacsList2

  putStrLn $ (show res1) ++ "  " ++ (show res2)

Question: How can I change the above example to run the two sat calls in parallel, i.e., using concurrency? I am interested in performance, if there are different options.

(Just to check: As I understand it, the ST monad is orthogonal and cannot be used in conjunction with parallelization/concurrency. The ST monad confused me a bit in the beginning, is is one of the reasons I ask the question.)

Solution

  • The easiest approach is to use the async library. Something like this, maybe.

    [res1, res2] <- mapConcurrently solve [dimacsList1, dimacsList2]