From a42869d36c1dc85c2f41d405a5800e2e6992a2df Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Mon, 25 Apr 2016 15:15:56 +0200
Subject: FSV 02 H2-1
---
ss2016/fsv/02/H2-1.hs | 76 ++++++++++++++++++++++++++++++++++++++++++++++++++
ss2016/fsv/02/manifest | 1 +
2 files changed, 77 insertions(+)
create mode 100644 ss2016/fsv/02/H2-1.hs
create mode 100644 ss2016/fsv/02/manifest
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
--
cgit v1.2.3