Satyros.DPLL.StorageUtil

Documentation

assignDecisionVariable :: Functor f => Literal -> DPLL s f ()

assignImplicationVariable :: Functor f => Literal -> Clause -> DPLL s f ()

assignFailureDrivenVariable :: Functor f => Literal -> Clause -> DPLL s f ()

eraseCurrentImplicationVariables :: Functor f => DPLL s f ()

learnClause :: Functor f => Clause -> DPLL s f ()

dropLevel :: Functor f => DPLL s f (Maybe (Maybe Variable, Set Variable))

dropIrrelevantLevels :: Functor f => Clause -> DPLL s f ()

deriveConflictClauseRelSAT :: Functor f => Clause -> DPLL s f Clause

levelToSet :: (Maybe Variable, Set Variable) -> Set Variable