FSV 02 H2-1

2 files changed, 77 insertions, 0 deletions

diff --git a/ss2016/fsv/02/H2-1.hs b/ss2016/fsv/02/H2-1.hs
new file mode 100644
index 0000000..8f83caf
--- /dev/null
+++ b/ss2016/fsv/02/H2-1.hs
@@ -0,0 +1,76 @@
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import Data.Map (Map)
+import Data.Set (Set)
+import Data.Maybe
+
+data Formula = Or [Formula]
+             | Not Formula
+             | Var Char
+
+type Assignment = Map Char Bool
+
+type CNFFormula = [Assignment -> Bool]
+
+satisfies :: Assignment -> CNFFormula -> Bool
+satisfies = all . flip ($)
+
+asCNF :: [Formula] -> CNFFormula
+asCNF = map asMap
+  where
+    -- asMap :: Formula -> (Assignment -> Bool)
+    asMap (Or xs) = \a -> any (($ a) . asMap) xs
+    asMap (Not x) = \a -> not $ (asMap x) a
+    asMap (Var x) = \a -> fromMaybe (error $ "Key " ++ [x] ++ " not in assignment") $ Map.lookup x a
+
+keys :: Formula -> Set Char
+keys (Or xs) = Set.unions $ map keys xs
+keys (Not x) = keys x
+keys (Var c) = Set.singleton c
+
+doDPLL :: CNFFormula -> [Char] -> Maybe Assignment
+doDPLL [] _ = Just Map.empty
+doDPLL _ [] = Just Map.empty
+doDPLL f keys = doDPLL' as f
+  where
+    as = map (Map.fromList . zip keys) . takeWhile ((== length keys) . length) . dropWhile ((< length keys) . length) $ bs
+    bs = [[True], [False]] ++ [ head : tail | tail <- bs, head <- [True, False] ]
+    doDPLL' [] f = Nothing
+    doDPLL' (a:as) f
+      | a `satisfies` f = Just a
+      | otherwise = doDPLL' as f
+
+main = do
+  let
+    fs = [ Var 'D'
+         , Or [ Not $ Var 'D'
+              , Not $ Var 'A'
+              , Var 'B'
+              ]
+         , Or [ Not $ Var 'B'
+              , Not $ Var 'E'
+              ]
+         , Or [ Var 'E'
+              , Var 'A'
+              , Not $ Var 'D'
+              ]
+         , Or [ Not $ Var 'F'
+              , Var 'G'
+              ]
+         , Or [ Not $ Var 'G'
+              , Not $ Var 'D'
+              , Not $ Var 'C'
+              ]
+         , Or [ Var 'C'
+              , Not $ Var 'H'
+              ]
+         , Or [ Var 'H'
+              , Var 'F'
+              ]
+         , Or [ Var 'D'
+              , Var 'A'
+              , Var 'B'
+              ]
+         ]
+  print $ doDPLL (asCNF fs) (Set.toList . Set.unions $ map keys fs)
+  -- Just (fromList [('A',False),('B',False),('C',True),('D',True),('E',True),('F',False),('G',False),('H',True)])
diff --git a/ss2016/fsv/02/manifest b/ss2016/fsv/02/manifest
new file mode 100644
index 0000000..51f6d31
--- /dev/null
+++ b/ss2016/fsv/02/manifest
@@ -0,0 +1 @@
+H2-1.hs
\ No newline at end of file