Satyros.DPLL.BCP

Documentation

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

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

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