-- |
-- Module      : AutoProof.Internal.Classical.SAT.Algorithms.DPLL
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- DPLL satisfiability algorithm.
module AutoProof.Internal.Classical.SAT.Algorithms.DPLL
  ( satDPLL,
    satAssignmentDPLL,
  )
where

import AutoProof.Internal.Classical.CNF (CNF)
import qualified AutoProof.Internal.Classical.CNF as CNF
  ( fromFormula,
    getAnyLiteral,
    pureLiteral,
    substitute,
    substitutePure,
    unitLiteral,
  )
import AutoProof.Internal.Formula (Formula)
import Control.Applicative ((<|>))
import Data.Map (Map)
import qualified Data.Map as Map (empty, insert, null)
import Data.Maybe (isJust)
import qualified Data.Set as Set

-- | DPLL satisfiability algorithm.
--
-- ==== __Examples__
--
-- >>> import AutoProof.Internal.Formula
-- >>> satDPLL $ Var "a"
-- True
--
-- >>> satDPLL $ And (Var "a") (Not (Var "a"))
-- False
satDPLL :: Ord a => Formula a -> Bool
satDPLL :: Formula a -> Bool
satDPLL = Maybe (Map a Bool) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Map a Bool) -> Bool)
-> (Formula a -> Maybe (Map a Bool)) -> Formula a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> Maybe (Map a Bool)
forall a. Ord a => Formula a -> Maybe (Map a Bool)
satAssignmentDPLL

-- | DPLL satisfiability algorithm, returning a satisfying truth assihnment, if
-- there is one.
--
-- ==== __Examples__
--
-- >>> a = And (Not (Var "a")) (Or (Var "b") (Var "c")) -- satisfiable
-- >>> Just t = satAssignmentDPLL a
-- >>> t
-- fromList [("a",False),("c",True)]
-- >>> t |= a
-- True
--
-- /Note:/ The variable @"b"@ is missing in the map above, which means that it's
-- implictly assigned the value 'False'.
--
-- >>> satAssignmentDPLL $ And (Var "a") (Not (Var "a")) -- unsatisfiable
-- Nothing
satAssignmentDPLL :: Ord a => Formula a -> Maybe (Map a Bool)
satAssignmentDPLL :: Formula a -> Maybe (Map a Bool)
satAssignmentDPLL = CNF a -> Maybe (Map a Bool)
forall a. Ord a => CNF a -> Maybe (Map a Bool)
satAssignmentDPLLFromCNF (CNF a -> Maybe (Map a Bool))
-> (Formula a -> CNF a) -> Formula a -> Maybe (Map a Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> CNF a
forall a. Ord a => Formula a -> CNF a
CNF.fromFormula

satAssignmentDPLLFromCNF :: Ord a => CNF a -> Maybe (Map a Bool)
satAssignmentDPLLFromCNF :: CNF a -> Maybe (Map a Bool)
satAssignmentDPLLFromCNF = Map a Bool -> CNF a -> Maybe (Map a Bool)
forall a. Ord a => Map a Bool -> CNF a -> Maybe (Map a Bool)
solve Map a Bool
forall k a. Map k a
Map.empty
  where
    solve :: Map a Bool -> CNF a -> Maybe (Map a Bool)
solve m :: Map a Bool
m cnf :: CNF a
cnf
      | CNF a -> Bool
forall a. Set a -> Bool
Set.null CNF a
cnf = Map a Bool -> Maybe (Map a Bool)
forall a. a -> Maybe a
Just Map a Bool
m
      | (Map a Bool -> Bool) -> CNF a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Map a Bool -> Bool
forall k a. Map k a -> Bool
Map.null CNF a
cnf = Maybe (Map a Bool)
forall a. Maybe a
Nothing
      | Bool
otherwise =
        case CNF a -> Maybe (Literal a)
forall a. CNF a -> Maybe (Literal a)
CNF.unitLiteral CNF a
cnf of
          Just (x :: a
x, b :: Bool
b) -> Map a Bool -> CNF a -> Maybe (Map a Bool)
solve (a -> Bool -> Map a Bool -> Map a Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
x Bool
b Map a Bool
m) (CNF a -> a -> Bool -> CNF a
forall a. Ord a => CNF a -> a -> Bool -> CNF a
CNF.substitute CNF a
cnf a
x Bool
b)
          Nothing -> case CNF a -> Maybe (Literal a)
forall a. Ord a => CNF a -> Maybe (Literal a)
CNF.pureLiteral CNF a
cnf of
            Just (x :: a
x, b :: Bool
b) -> Map a Bool -> CNF a -> Maybe (Map a Bool)
solve (a -> Bool -> Map a Bool -> Map a Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
x Bool
b Map a Bool
m) (CNF a -> a -> Bool -> CNF a
forall a. Ord a => CNF a -> a -> Bool -> CNF a
CNF.substitutePure CNF a
cnf a
x Bool
b)
            Nothing -> case CNF a -> Maybe (Literal a)
forall a. CNF a -> Maybe (Literal a)
CNF.getAnyLiteral CNF a
cnf of
              Nothing -> Maybe (Map a Bool)
forall a. Maybe a
Nothing -- should be unreachable
              Just (x :: a
x, _) ->
                Map a Bool -> CNF a -> Maybe (Map a Bool)
solve (a -> Bool -> Map a Bool -> Map a Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
x Bool
True Map a Bool
m) (CNF a -> a -> Bool -> CNF a
forall a. Ord a => CNF a -> a -> Bool -> CNF a
CNF.substitute CNF a
cnf a
x Bool
True)
                  Maybe (Map a Bool) -> Maybe (Map a Bool) -> Maybe (Map a Bool)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Map a Bool -> CNF a -> Maybe (Map a Bool)
solve (a -> Bool -> Map a Bool -> Map a Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
x Bool
False Map a Bool
m) (CNF a -> a -> Bool -> CNF a
forall a. Ord a => CNF a -> a -> Bool -> CNF a
CNF.substitute CNF a
cnf a
x Bool
False)