Skip to content

Instantly share code, notes, and snippets.

@deque-blog deque-blog/AllOfSat.hs
Last active Aug 26, 2017

Embed
What would you like to do?
module SAT where
import Control.Monad
import qualified Data.Map as Map
import qualified Data.Set as Set
type Var = String
type Assignment = [(Var, Bool)]
data Term
= Pos { getVar :: String }
| Neg { getVar :: String }
newtype SAT = SAT { conjunctions :: [[Term]]}
sat :: SAT -> Maybe Assignment
sat pb = headSafe $ do
assignment <- forM (allVars pb) $ \var -> do
val <- [True, False]
pure (var, val)
guard (evalSat assignment pb)
pure assignment
allVars :: SAT -> [Var]
allVars = Set.toList . Set.fromList . map getVar . concat . conjunctions
evalSat :: Assignment -> SAT -> Bool
evalSat assignment =
let env = Map.fromList assignment
in and . map (any (evalTerm env)) . conjunctions
evalTerm :: Map.Map Var Bool -> Term -> Bool
evalTerm env (Pos var) = env Map.! var
evalTerm env (Neg var) = not (env Map.! var)
------------------------------------------------------------
headSafe :: [a] -> Maybe a
headSafe [] = Nothing
headSafe xs = Just (head xs)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.