From 3a62fd2363e4fde38ddf62ec079d7e9dd659967a Mon Sep 17 00:00:00 2001 From: Dimitri Lozeve Date: Wed, 3 Aug 2016 19:30:43 +0100 Subject: [PATCH] Resolution rule: finding suitable pairs of clauses --- Sat.hs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/Sat.hs b/Sat.hs index 7fa2f99..bedfc29 100644 --- a/Sat.hs +++ b/Sat.hs @@ -145,6 +145,25 @@ resolve a b = do x <- commonVar a b return $ (a \\ [x, notLit x]) `union` (b \\ [x, notLit x]) +-- Given a formula and a clause, returns a clause which can be reduced +-- with the first one by applying the resolution rule. +findMatchingClause :: CNF -> Clause -> Maybe Clause +findMatchingClause _ [] = Nothing +findMatchingClause f (x:xs) = + case find (elem $ notLit x) f of + Nothing -> findMatchingClause f xs + Just c -> Just c + +-- Returns a two clauses suitable for the resolution rule, if +-- possible. +findMatchingPair :: CNF -> Maybe (Clause, Clause) +findMatchingPair [] = Nothing +findMatchingPair (c:cs) = + case findMatchingClause cs c of + Nothing -> findMatchingPair cs + Just d -> Just (c, d) + + ----------------------------------------------------------------------