568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedermodule GMPSAT where

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederimport qualified Data.Set as Set

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederimport GMPAS

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- SAT Decidability Algorithm

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- The folowing is a sketch of the algorithm and will need

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- many other auxiliary things

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder{-

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedercheckSAT = do f <- par5er

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ; H <- guessPV f

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ; Ro = chooseCC H

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ; R = chooseRC Ro

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ; c = guessClause R

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ; res = checkSAT c R Ro

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ; return res

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-}

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- 1. Guess Pseudovaluation H for f -- genPV

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederguessPV :: (Ord t) => Formula t -> [Set.Set (TVandMA t)]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederguessPV f =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder let l = genPV f

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in filter (eval f) l

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- modify the set of truth values / generate the next truth values set --------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenTV :: (Ord t) => Set.Set (TVandMA t) -> Set.Set (TVandMA t)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenTV s =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder let

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder (TVandMA (x,t),y) = Set.deleteFindMin s

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in if (t == False)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then (Set.insert (TVandMA (x,True)) y)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else if (y == Set.empty)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then Set.empty

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else let

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder aux = genTV(y)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in if (aux == Set.empty)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then Set.empty

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else (Set.insert (TVandMA (x,False)) aux)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- generate a list with all Pseudovaluations of a formula ---------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenPV :: (Eq t, Ord t) => Formula t -> [Set.Set (TVandMA t)]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenPV f =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder let aux = setMA f

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in if (aux == Set.empty)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then aux:[]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else let recMakeList s =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder let nextset = genTV s

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in if (nextset == Set.empty)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then []

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else (nextset:(recMakeList nextset))

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in (aux:(recMakeList aux))

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- Junctor evaluation ---------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederjmap :: Junctor -> Bool -> Bool -> Bool

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederjmap j x y =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder case j of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder And -> and([x,y])

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Or -> or([x,y])

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder If -> or([not(x),y])

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Fi -> or([x,not(y)])

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Iff -> and([or([not(x),y]),or([x,not(y)])])

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- Formula Evaluation with truth values provided by the TVandMA set -----------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedereval :: (Eq a) => (Formula a) -> Set.Set (TVandMA a) -> Bool

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedereval f ts =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder case f of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder T -> True

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder F -> False

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Neg f1 -> not(eval f1 ts)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Junctor f1 j f2 -> (jmap j (eval f1 ts) (eval f2 ts))

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Mapp i f1 -> let findInS s ff =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder if (s == Set.empty)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then False -- this could very well be True

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else let (TVandMA (x,t),y) = Set.deleteFindMin s

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in if (x == ff)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then t

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else findInS y ff

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder findInS ts (Mapp i f1)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- make (Truth Values, Modal Atoms) set from Formula f ------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedersetMA :: (Ord t) => Formula t -> Set.Set (TVandMA t)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedersetMA f =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder case f of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder T -> Set.empty

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder F -> Set.empty

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Neg f1 -> setMA f1

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Junctor f1 _ f2 -> Set.union (setMA f1) (setMA f2)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Mapp i f1 -> Set.insert (TVandMA (Mapp i f1,False)) Set.empty

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- 2. Choose a ctr. cl. Ro /= F over MA(H) s.t. H "entails" ~Ro -- genAllLists

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- reverse the truth values of the set elements -------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederrevTV :: (Ord t, Eq t) => Set.Set (TVandMA t) -> Set.Set (TVandMA t)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederrevTV s = if (s == Set.empty)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then Set.empty

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else let (TVandMA (x,t),aux) = Set.deleteFindMin s

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in Set.insert (TVandMA (x,not(t))) (revTV aux)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- return the list of sets of n choose k of the set s -------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedernck :: (Ord t) => Set.Set (TVandMA t) -> Int -> Int -> [Set.Set (TVandMA t)]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedernck s n k =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder case (n-k) of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder 0 -> [revTV s]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder _ ->

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder case k of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder 0 -> [Set.empty]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder _ -> let (TVandMA (x,t),aux) = Set.deleteFindMin s

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in (map (Set.insert (TVandMA (x,not(t)))) (nck aux (n-1) (k-1)))

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ++ (nck aux (n-1) k)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- generate all unpermuted sets of size <= n of the set s ---------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenAllSets :: (Ord t) => Set.Set (TVandMA t) -> Int -> [Set.Set (TVandMA t)]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenAllSets s n =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder case n of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder 0 -> []

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder _ -> let size = Set.size s

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in (nck s size n) ++ (genAllSets s (n-1))

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- for testing purposes -------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedertest :: (Ord t) => Set.Set (TVandMA t) -> [[TVandMA t]]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedertest s = let l = genAllSets s (Set.size s)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in genAllLists l

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- return the list of lists -> permutations of a set --------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederperm :: (Ord t) => Set.Set t -> [[t]]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederperm s =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder if (Set.size s <= 1)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder then [Set.toList s]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder else let (x,aux1) = Set.deleteFindMin s

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder (y,aux2) = Set.deleteFindMin aux1

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder in map (x:) (perm aux1) ++ map (y:) (perm (Set.insert x aux2))

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- generates all lists of RO's out of a given pseudovaluation s ---------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenAllLists :: (Ord t) => [Set.Set t] -> [[t]]

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaedergenAllLists l =

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder case l of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder [] -> []

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder _ -> (perm (head l)) ++ (genAllLists (tail l))

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- 5. Recursively check that ~c(R,Ro) is satisfiable.

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- checkS

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-------------------------------------------------------------------------------

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder