module Ersatz.Solver.Toysat where
import Control.Monad
import Control.Monad.IO.Class
import Data.Array.IArray
import qualified Data.Foldable as F
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Ersatz
import qualified ToySolver.SAT as ToySAT
toysat :: MonadIO m => Solver SAT m
toysat problem = liftIO $ do
solver <- ToySAT.newSolver
let nv = dimacsNumVariables problem
ToySAT.newVars_ solver nv
F.forM_ (dimacsClauses problem) $ \clause -> do
ToySAT.addClause solver (IntSet.toList clause)
ret <- ToySAT.solve solver
if ret then do
model <- ToySAT.getModel solver
return (Satisfied, IntMap.fromList (assocs model))
else
return (Unsatisfied, IntMap.empty)