From f0ab796149ca4a10f8684af3aa75abcff6ef4a8a Mon Sep 17 00:00:00 2001
From: Dimitri Lozeve <dimitri.lozeve@gmail.com>
Date: Wed, 3 Aug 2016 19:17:38 +0100
Subject: [PATCH] Resolution rule: basic functions

---
 Sat.hs | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Sat.hs b/Sat.hs
index 1d783c5..7fa2f99 100644
--- a/Sat.hs
+++ b/Sat.hs
@@ -129,6 +129,22 @@ unitPropagate (f, asst) =
       _ -> unitPropagate (eliminateUnits units f, asst `union` units)
 
 
+-- Resolution
+
+-- Returns the first common variable between two clauses, if it exists
+commonVar :: Clause -> Clause -> Maybe Lit
+commonVar _ [] = Nothing
+commonVar as (b:bs) = if b `elem` as || notLit b `elem` as
+                      then Just b
+                      else commonVar as bs
+
+-- Applies the resolution rule to two clauses sharing a variable. This
+-- function does not test whether the literals are of different sign.
+resolve :: Clause -> Clause -> Maybe Clause
+resolve a b = do
+  x <- commonVar a b
+  return $ (a \\ [x, notLit x]) `union` (b \\ [x, notLit x])
+
 
 ----------------------------------------------------------------------