1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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)])
|
