-- |
-- Module      : AutoProof.Internal.Classical.SAT.Algorithms.Simple
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- A simple baseline SAT algorithm.
module AutoProof.Internal.Classical.SAT.Algorithms.Simple
  ( satSimple,
    satAssignmentSimple,
  )
where

import AutoProof.Internal.Classical.SAT.TruthAssignment
  ( TruthAssignment (evalFormula),
  )
import AutoProof.Internal.Formula (Formula (Lit), getAnyVariable, substitute)
import Control.Applicative ((<|>))
import Data.Map (Map)
import qualified Data.Map as Map

-- | A simple baseline satisfiability algorithm.
--
-- This algorithm is based on the observation that if \(a\) is a propositional
-- formula and \(x\) is a propositional variable, then \(a\) is satisfiable if
-- and only if either \(a[\top/x]\) is satisfiable or \(a[\bot/x]\) is
-- satisfiable.
--
-- ==== __Examples__
--
-- >>> satSimple $ Var "a"
-- True
--
-- >>> satSimple $ And (Var "a") (Not (Var "a"))
-- False
satSimple :: Eq a => Formula a -> Bool
satSimple :: Formula a -> Bool
satSimple a :: Formula a
a = case Formula a -> Maybe a
forall a. Formula a -> Maybe a
getAnyVariable Formula a
a of
  Nothing -> () -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula () Formula a
a
  Just x :: a
x ->
    Formula a -> Bool
forall a. Eq a => Formula a -> Bool
satSimple (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
True))
      Bool -> Bool -> Bool
|| Formula a -> Bool
forall a. Eq a => Formula a -> Bool
satSimple (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False))

-- | A simple baseline satisfiability algorithm, returning a satisfying truth
-- assignment if there is one.
--
-- This algorithm is based on the observation that if \(a\) is a propositional
-- formula and \(x\) is a propositional variable, then \(a\) is satisfiable if
-- and only if either \(a[\top/x]\) is satisfiable or \(a[\bot/x]\) is
-- satisfiable.
--
-- ==== __Examples__
--
-- >>> a = And (Not (Var "a")) (Or (Var "b") (Var "c")) -- satisfiable
-- >>> Just t = satAssignmentSimple a
-- >>> t
-- fromList [("a",False),("b",True),("c",True)]
-- >>> t |= a
-- True
--
-- >>> satAssignmentSimple $ And (Var "a") (Not (Var "a")) -- unsatisfiable
-- Nothing
satAssignmentSimple :: Ord a => Formula a -> Maybe (Map a Bool)
satAssignmentSimple :: Formula a -> Maybe (Map a Bool)
satAssignmentSimple = Map a Bool -> Formula a -> Maybe (Map a Bool)
forall a. Ord a => Map a Bool -> Formula a -> Maybe (Map a Bool)
solve Map a Bool
forall k a. Map k a
Map.empty
  where
    solve :: Map a Bool -> Formula a -> Maybe (Map a Bool)
solve m :: Map a Bool
m a :: Formula a
a = case Formula a -> Maybe a
forall a. Formula a -> Maybe a
getAnyVariable Formula a
a of
      Nothing -> if () -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula () Formula a
a then Map a Bool -> Maybe (Map a Bool)
forall a. a -> Maybe a
Just Map a Bool
m else Maybe (Map a Bool)
forall a. Maybe a
Nothing
      Just x :: a
x ->
        Map a Bool -> Formula 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) (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x (Bool -> Formula a
forall a. Bool -> Formula a
Lit 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 -> Formula 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) (Formula a -> a -> Formula a -> Formula a
forall a. Eq a => Formula a -> a -> Formula a -> Formula a
substitute Formula a
a a
x (Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False))