module Funsat.Resolution
(
checkDepthFirst
, ResolutionTrace(..)
, initResolutionTrace
, ResolutionError(..)
, UnsatisfiableCore )
where
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State.Strict
import Data.IntSet( IntSet )
import Data.List( nub )
import Data.Map( Map )
import qualified Data.IntSet as IntSet
import qualified Data.Map as Map
import Funsat.Types
import Funsat.Utils( isSingle, getUnit, isFalseUnder )
data ResolutionTrace = ResolutionTrace
{ traceFinalClauseId :: ClauseId
, traceFinalAssignment :: IAssignment
, traceSources :: Map ClauseId [ClauseId]
, traceOriginalClauses :: Map ClauseId Clause
, traceAntecedents :: Map Var ClauseId }
deriving (Show)
initResolutionTrace finalClauseId finalAssignment = ResolutionTrace
{ traceFinalClauseId = finalClauseId
, traceFinalAssignment = finalAssignment
, traceSources = Map.empty
, traceOriginalClauses = Map.empty
, traceAntecedents = Map.empty }
data ResolutionError =
ResolveError Var Clause Clause
| CannotResolve [Var] Clause Clause
| AntecedentNotUnit Clause
| AntecedentImplication (Clause, Lit) Var
| AntecedentMissing Var
| EmptySource ClauseId
| OrphanSource ClauseId
deriving Show
instance Error ResolutionError where
checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore
checkDepthFirst resTrace =
fmap (map findClause . IntSet.toList)
. (`runReader` resTrace)
. (`evalStateT` ResState { clauseIdMap = traceOriginalClauses resTrace
, unsatCore = IntSet.empty })
. runErrorT
$ recursiveBuild (traceFinalClauseId resTrace)
>>= checkDFClause
where
findClause clauseId =
Map.findWithDefault
(error $ "checkDFClause: unoriginal clause id: " ++ show clauseId)
clauseId (traceOriginalClauses resTrace)
type UnsatisfiableCore = [Clause]
data ResState = ResState
{ clauseIdMap :: Map ClauseId Clause
, unsatCore :: UnsatCoreIntSet }
type UnsatCoreIntSet = IntSet
type ResM = ErrorT ResolutionError (StateT ResState (Reader ResolutionTrace))
checkDFClause :: Clause -> ResM UnsatCoreIntSet
checkDFClause clause =
if null clause
then gets unsatCore
else do l <- chooseLiteral clause
let v = var l
anteClause <- recursiveBuild =<< getAntecedentId v
checkAnteClause v anteClause
resClause <- resolve (Just v) clause anteClause
checkDFClause resClause
recursiveBuild :: ClauseId -> ResM Clause
recursiveBuild clauseId = do
maybeClause <- getClause
case maybeClause of
Just clause -> return clause
Nothing -> do
sourcesMap <- asks traceSources
case Map.lookup clauseId sourcesMap of
Nothing -> throwError (OrphanSource clauseId)
Just [] -> throwError (EmptySource clauseId)
Just (firstSourceId:ids) -> recursiveBuildIds clauseId firstSourceId ids
where
getClause = do
origMap <- asks traceOriginalClauses
case Map.lookup clauseId origMap of
Just origClause -> withClauseInCore $ return (Just origClause)
Nothing -> Map.lookup clauseId `liftM` gets clauseIdMap
withClauseInCore =
(modify (\s -> s{ unsatCore = IntSet.insert clauseId (unsatCore s) }) >>)
recursiveBuildIds clauseId firstSourceId sourceIds = do
rc <- recursiveBuild firstSourceId
clause <- foldM buildAndResolve rc sourceIds
storeClauseId clauseId clause
return clause
where
buildAndResolve :: Clause -> ClauseId -> ResM (Clause)
buildAndResolve clause1 clauseId =
recursiveBuild clauseId >>= resolve Nothing clause1
storeClauseId :: ClauseId -> Clause -> ResM ()
storeClauseId clauseId clause = modify $ \s ->
s{ clauseIdMap = Map.insert clauseId clause (clauseIdMap s) }
resolve :: Maybe Var -> Clause -> Clause -> ResM Clause
resolve maybeV c1 c2 =
case filter ((`elem` c2) . negate) c1 of
[l] -> case maybeV of
Nothing -> resolveVar (var l)
Just v -> if v == var l
then resolveVar v
else throwError $ ResolveError v c1 c2
vs -> throwError $ CannotResolve (nub . map var $ vs) c1 c2
where
resolveVar v = return . nub $ deleteVar v c1 ++ deleteVar v c2
deleteVar v c = c `without` lit v `without` negate (lit v)
lit (V i) = L i
getAntecedentId :: Var -> ResM ClauseId
getAntecedentId v = do
anteMap <- asks traceAntecedents
case Map.lookup v anteMap of
Nothing -> throwError (AntecedentMissing v)
Just ante -> return ante
chooseLiteral :: Clause -> ResM Lit
chooseLiteral (l:_) = return l
chooseLiteral _ = error "chooseLiteral: empty clause"
checkAnteClause :: Var -> Clause -> ResM ()
checkAnteClause v anteClause = do
a <- asks traceFinalAssignment
when (not (anteClause `hasUnitUnder` a))
(throwError $ AntecedentNotUnit anteClause)
let unitLit = getUnit anteClause a
when (not $ var unitLit == v)
(throwError $ AntecedentImplication (anteClause, unitLit) v)
where
hasUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c)