module CombinatorialOptimisation.SAT(
SATProblem(SATProblem,numClauses,numSATEDClauses,numVariables,variableLookUp,variablePosition,clausePosition,clauseLookUp),
numUnSATEDClauses,getTrueFalseCount,summariseSAT,makeRandomSATProblem,flipVariable,satproblem,setAllVars,randomiseVariables
)where
import qualified Data.IntMap as IM
import qualified Data.Array as A
import Data.List
import System.Random
import System.IO.Unsafe
import Data.Char
data SATProblem = SATProblem { numClauses :: Int,
numSATEDClauses :: Int,
numVariables :: Int,
variableLookUp :: Int->([Int],[Int]),
clauseLookUp :: Int->([Int],[Int]),
variablePosition :: IM.IntMap Bool,
clausePosition :: IM.IntMap Int}
instance Eq SATProblem where
(==) s1 s2 = (numSATEDClauses s1) == (numSATEDClauses s2) && (variablePosition s1) == (variablePosition s2)
instance Ord SATProblem where
compare s1 s2 = compare (numSATEDClauses s2) (numSATEDClauses s1)
instance Show SATProblem where
show s = showSATLogic s ++"\n"++ showVARPosition s ++"\n"++ summariseSAT s++"\n"++(show $ getTrueFalseCount s)
getTrueFalseCount :: SATProblem->(Int,Int)
getTrueFalseCount s = let ls = IM.elems $ variablePosition s
in (length (filter (==True) ls),length (filter (==False) ls))
numUnSATEDClauses :: SATProblem->Int
numUnSATEDClauses s = numClauses s numSATEDClauses s
showSATLogic :: SATProblem->String
showSATLogic s = concat (intersperse " /\\\n" (map writeClause [0 .. numClauses s 1])) ++ "\n"
where
writeClause c = let (as,bs) = clauseLookUp s c
(as',bs') = (map (\a->(a,' ')) as,map (\a->(a,'!')) bs)
cs = sortBy (\a b->compare (fst a) (fst b)) $ as' ++ bs'
in '(' : (concat $ intersperse " \\/ " $ [ d :'x':show c | (c,d)<-cs]) ++ ")"
summariseSAT :: SATProblem->String
summariseSAT s = concat ["number of clauses : ",show (numClauses s),"\n",
"number of variables : ",show (numVariables s),"\n",
"satisfied clauses : ",show (numSATEDClauses s),"\n",
satMessage,"\n"]
where
sat = (numSATEDClauses s) == (numClauses s)
satMessage = if sat then "SATisfied" else "unSATisfied"
showVARPosition :: SATProblem->String
showVARPosition s = concat [concat [" x",show v," = ",show t,"\n" ] |(v,t)<- IM.assocs (variablePosition s)]
satproblem :: Int->Int->(Int->([Int],[Int]))->(Int->([Int],[Int]))->IM.IntMap Bool->SATProblem
satproblem nClauses nVars varLookup claLookup varPosition
= SATProblem nClauses satClause nVars varLookup claLookup varPosition finalClausePosition
where
varList = [0 .. nVars 1]
initialClausePositions = IM.fromList $ zip [0 .. nClauses 1] $ repeat 0
finalClausePosition = foldl f IM.empty [0 .. nVars 1]
f m v = let (ords,negs) = varLookup v
varPos = varPosition IM.! v
in if varPos then foldl (\m' c->IM.adjust (+1) c m') m ords else foldl (\m' c->IM.adjust (+1) c m') m negs
satClause = sum $ map (\x->if x ==0 then 0 else 1) (IM.elems finalClausePosition)
setAllVars :: Bool->SATProblem->SATProblem
setAllVars b s = satproblem (numClauses s) (numVariables s) (variableLookUp s) (clauseLookUp s) initialVarPosition
where
initialVarPosition = IM.fromList $ zip [0 .. numVariables s 1] $ repeat b
randomiseVariables :: RandomGen g=>g->SATProblem->SATProblem
randomiseVariables g s = satproblem (numClauses s) (numVariables s) (variableLookUp s) (clauseLookUp s) varpos
where
varpos = IM.fromList $ zip [0 .. (numVariables s) 1] $ (randoms g :: [Bool])
makeRandomSATProblem :: RandomGen g=>g->Int->Int->SATProblem
makeRandomSATProblem gen numVariables numClauses
= satproblem numClauses numVariables varLookup claLookup initialVarPosition
where
initialVarPosition = IM.fromList $ zip [0 .. numVariables 1] $ repeat False
clauses = take numClauses $ nub (unfoldr generateRandomClause gen)
generateRandomClause g = let f (ms,ns) gen'
| length ms + length ns == 3 = (ms,ns,gen')
| otherwise = let (l :: Int,gen'') = randomR (0,1) gen'
(n :: Int,gen''') = randomR (0,numVariables 1) gen''
already = elem n ms || elem n ns
in if already then f (ms,ns) gen'''
else if l ==0 then f (n:ms,ns) gen'''
else f (ms,n:ns) gen'''
(ords,negs,g') = f ([],[]) g
in Just ((sort ords,sort negs),g')
emptyClauseData = IM.fromList $ zip [0 .. numVariables 1] (repeat ([],[]))
basicClauseLookup = foldl constructClauseLookup emptyClauseData $ zip [0..] clauses
varLookup = ((A.listArray (0,numVariables1) (IM.elems basicClauseLookup)) A.!)
constructClauseLookup m (clauseIndex,(ords,negs)) = let addNeg m' x = IM.adjust (\(as,bs)->(as,clauseIndex:bs)) x m'
addOrd m' x = IM.adjust (\(as,bs)->(clauseIndex:as,bs)) x m'
in foldl addNeg (foldl addOrd m ords) negs
claLookup = ((A.listArray (0,numVariables1) clauses) A.!)
flipVariable :: Int->SATProblem->(SATProblem,Int)
flipVariable v s
= let modifiedVarPos = IM.insert v changedVar (variablePosition s)
in (s{numSATEDClauses=numSATEDClauses s + overAllChange,variablePosition=modifiedVarPos,clausePosition=modifiedClausePos},overAllChange)
where
overAllChange = ordChange + negChange
changedVar = not $ (variablePosition s) IM.! v
(ords,negs) = (variableLookUp s) v
cp = clausePosition s
(cp',ordChange) = if changedVar then foldl countInc (cp,0) ords else foldl countDec (cp,0) ords
(modifiedClausePos,negChange) = if changedVar then foldl countDec (cp',0) negs else foldl countInc (cp',0) negs
countInc (positions,counter) i = let current = positions IM.! i
counter' = if current == 0 then counter+1 else counter
in (IM.insert i (current+1) positions,counter')
countDec (positions,counter) i = let current = positions IM.! i
counter' = if current == 1 then counter1 else counter
in (IM.insert i (current1) positions,counter')