From d140723b26681a9ee3d41c9e331f3bbba7e6f6c5 Mon Sep 17 00:00:00 2001 From: Dimitri Lozeve Date: Tue, 2 Aug 2016 20:51:32 +0100 Subject: [PATCH] Unit propagation rule --- Sat.hs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Sat.hs b/Sat.hs index 1fffb39..0a62e65 100644 --- a/Sat.hs +++ b/Sat.hs @@ -114,6 +114,21 @@ pureLitRule (f, asst) = (f', asst ++ pures) f' = foldr (eliminatePure . fromLit) f pures +-- Unit Propagation + +-- Evaluates the formula with all the unit clauses given in argument +eliminateUnits :: [Lit] -> CNF -> CNF +eliminateUnits xs f = foldr evalLit f xs + +-- Applies the unit propagation rule +unitPropagate :: (CNF, Assignment) -> (CNF, Assignment) +unitPropagate (f, asst) = + let units = concat $ filter (\xs -> length xs == 1) f in + case units of + [] -> (f, asst) + _ -> unitPropagate (eliminateUnits units f, asst `union` units) + + ----------------------------------------------------------------------