acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedermodule GMPSAT where

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

3a6c7a7ff823616f56cd3d205fc44664a683effdChristian Maederimport qualified Data.Set as Set

73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian Maederimport GMPAS

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu-------------------------------------------------------------------------------

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder-- SAT Decidability Algorithm

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- many other auxiliary things

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-------------------------------------------------------------------------------

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski{-

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskicheckSAT = do f <- par5er

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ; H <- guessPV f

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ; Ro = chooseCC H

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ; R = chooseRC Ro

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ; c = guessClause R

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ; res = checkSAT c R Ro

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ; return res

85ebda7270c6883b503d3bde4757033c09c25644Christian Maeder-}

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-------------------------------------------------------------------------------

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- 1. Guess Pseudovaluation H for f -- genPV

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-------------------------------------------------------------------------------

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

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst SchulzguessPV f =

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder let l = genPV f

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz in filter (eval f) l

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- modify the set of truth values / generate the next truth values set --------

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedergenTV :: (Ord t) => Set.Set (TVandMA t) -> Set.Set (TVandMA t)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedergenTV s =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder let

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

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder in if (t == False)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder then (Set.insert (TVandMA (x,True)) y)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder else if (y == Set.empty)

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder then Set.empty

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder else let

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder aux = genTV(y)

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder in if (aux == Set.empty)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder then Set.empty

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

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder-- generate a list with all Pseudovaluations of a formula ---------------------

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedergenPV f =

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder let aux = setMA f

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder in if (aux == Set.empty)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder then aux:[]

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder else let recMakeList s =

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder let nextset = genTV s

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski in if (nextset == Set.empty)

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski then []

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski else (nextset:(recMakeList nextset))

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski in (aux:(recMakeList aux))

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- Junctor evaluation ---------------------------------------------------------

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskijmap :: Junctor -> Bool -> Bool -> Bool

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskijmap j x y =

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski case j of

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski And -> and([x,y])

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

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

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

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

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

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskieval :: (Eq a) => (Formula a) -> Set.Set (TVandMA a) -> Bool

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maedereval f s =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case f of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder T -> True

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder F -> False

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Neg f1 -> not(eval f1 s)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Junctor f1 j f2 -> (jmap j (eval f1 s) (eval f2 s))

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Mapp i f1 -> let findInS s ff =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder if (s == Set.empty)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder then False -- this could very well be True

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else let (TVandMA (x,t),y) = Set.deleteFindMin s

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in if (x == ff)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder then t

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else findInS y ff

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder findInS s (Mapp i f1)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- make (Truth Values, Modal Atoms) set from Formula f ------------------------

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedersetMA f =

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder case f of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder T -> Set.empty

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder F -> Set.empty

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Neg f1 -> setMA f1

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Junctor f1 j f2 -> Set.union (setMA f1) (setMA f2)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Mapp i f1 -> Set.insert (TVandMA (Mapp i f1,False)) Set.empty

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-------------------------------------------------------------------------------

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-------------------------------------------------------------------------------

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski-- reverse the truth values of the set elements -------------------------------

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till MossakowskirevTV :: (Ord t, Eq t) => Set.Set (TVandMA t) -> Set.Set (TVandMA t)

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till MossakowskirevTV s = if (s == Set.empty)

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski then Set.empty

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski else let (TVandMA (x,t),aux) = Set.deleteFindMin s

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski in Set.insert (TVandMA (x,not(t))) (revTV aux)

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski-- return the list of sets of n choose k of the set s -------------------------

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskinck :: (Ord t) => Set.Set (TVandMA t) -> Int -> Int -> [Set.Set (TVandMA t)]

b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettichnck s n k =

da955132262baab309a50fdffe228c9efe68251dCui Jian case (n-k) of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder 0 -> [revTV s]

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ ->

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder case k of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder 0 -> [Set.empty]

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

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ++ (nck aux (n-1) k)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- generate all unpermuted sets of size <= n of the set s ---------------------

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedergenAllSets s n =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder case n of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder 0 -> []

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> let size = Set.size s

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedertest s = let l = genAllSets s (Set.size s) -- for testing purposes

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz in genAllLists l

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz-- return the list of lists -> permutations of a set --------------------------

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzperm :: (Ord t) => Set.Set t -> [[t]]

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzperm s =

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz if (Set.size s <= 1)

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz then [Set.toList s]

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz else let (x,aux1) = Set.deleteFindMin s

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz (y,aux2) = Set.deleteFindMin aux1

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz in map (x:) (perm aux1) ++ map (y:) (perm (Set.insert x aux2))

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz-- generates all lists of RO's out of a given pseudovaluation s ---------------

295566c1778f463b624caf1be714b70d808e2a51Ewaryst SchulzgenAllLists :: (Ord t) => [Set.Set t] -> [[t]]

295566c1778f463b624caf1be714b70d808e2a51Ewaryst SchulzgenAllLists l =

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz case l of

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz [] -> []

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz _ -> (perm (head l)) ++ (genAllLists (tail l))

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz-------------------------------------------------------------------------------

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz-- 5. Recursively check that ~c(R,Ro) is satisfiable.

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz-- checkS

295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz-------------------------------------------------------------------------------

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz