module Satchmo.Solver.Funsat
( solve
)
where
import qualified Satchmo.Data
import qualified Satchmo.Solve
import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF
import qualified Funsat.Solver
import Funsat.Types
import Data.String
import Data.Array.Unboxed
import qualified Data.Map as M
import qualified Data.Set as S
solve = Satchmo.Solve.solve funsat
funsat :: Satchmo.Solve.Implementation
funsat cs = do
let Right cnf = ParseCNF.parseByteString "satchmo"
$ fromString cs
result @ ( sol, stats, mtrace ) = Funsat.Solver.solve1 $ asCNF cnf
case result of
( Funsat.Solver.Sat a, _, _ ) ->
return $ Just $ M.fromList $ do
l <- litAssignment a
return ( Satchmo.Data.literal $ abs $ unLit l, litSign l )
_ -> return Nothing
asCNF :: ParseCNF.CNF -> CNF
asCNF (ParseCNF.CNF v c is) =
CNF { numVars = v
, numClauses = c
, clauses = S.fromList . map (map fromIntegral . elems) $ is
}