Satisfiability, second attempt

Satisfy.hs

{-# LANGUAGE NoImplicitPrelude #-}
--
-- <http://en.wikipedia.org/wiki/Boolean_satisfiability_problem>
--
-- In complexity theory, the satisfiability problem (SAT) is a decision 
-- problem, whose instance is a Boolean expression written using only 
-- AND, OR, NOT, variables, and parentheses. The question is: given the 
-- expression, is there some assignment of TRUE and FALSE values to the 
-- variables that will make the entire expression true? A formula of 
-- propositional logic is said to be satisfiable if logical values can 
-- be assigned to its variables in a way that makes the formula true. 
--
-- The Boolean satisfiability problem is NP-complete. 
--
module Satisfy
    ( Expression(..)
    , Mapping
    , satisfy
    , negate
    , isSatisfiable
    , isNegatable
    ) where

import Prelude hiding (negate)
import Control.Arrow (second)
import qualified Data.Map as M

type Mapping = M.Map Int Bool

-- | A boolean expression with variables
data Expression = X Int          -- ^ x1,x2...xN
                | Pure Bool      -- ^ true or false (once assigned)
                | NOT Expression
                | Expression `AND` Expression
                | Expression `OR`  Expression

instance Show Expression where
    show (X i)         = 'x':show i
    show (Pure b)      = show b
    show (NOT  e)      = "!( " ++ show e  ++ " )"
    show (e1 `AND` e2) = "[ "  ++ show e1 ++ " && " ++ show e2 ++ " ]"
    show (e1 `OR`  e2) = "[ "  ++ show e1 ++ " || " ++ show e2 ++ " ]"

-- | Returns (Mapping, True) if the expression is satisfiable
--
--   > satisfy M.empty $ X 1 `AND` NOT (X 1)
--   > (fromList [(1,True)],False)
--
satisfy :: Mapping -> Expression -> (Mapping, Bool)
satisfy m (Pure b)      = (m, b)
satisfy m (NOT e)       = second not $ negate m e -- switch the result
satisfy m (e1 `AND` e2) = let (m', b) = satisfy m e1 in if b then satisfy m' e2 else (m, b)
satisfy m (e1 `OR`  e2) = let (m', b) = satisfy m e1 in if b then (m', b) else satisfy m e2
satisfy m (X i) =
    case M.lookup i m of
        Just b -> (m, b) -- variable's already known
        _      -> (M.insert i True m, True)

-- | Returns (Mapping, False) if the expression is negatable. We need to 
--   define both functions so that NOT expressions can be handled 
--   properly.
--
--   > negate M.empty $ X 1 `OR` NOT (X 1)
--   > (fromList [(1,False)],True)
--
negate :: Mapping -> Expression -> (Mapping, Bool)
negate m (Pure b)      = (m, b)
negate m (NOT e)       = second not $ satisfy m e -- switch the result
negate m (e1 `AND` e2) = let (m', b) = negate m e1 in if b then negate m e2 else (m', b)
negate m (e1 `OR`  e2) = let (m', b) = negate m e1 in if b then (m, b) else negate m' e2
negate m (X i) =
    case M.lookup i m of
        Just b -> (m, b) -- variable's already known
        _      -> (M.insert i False m, False)

-- | Apply a mapping to an expression yielding a new expression with the 
--   variables replaced accordingly
applyMapping :: Mapping -> Expression -> Expression
applyMapping _ (Pure b)      = Pure b
applyMapping m (NOT e)       = NOT $ applyMapping m e
applyMapping m (e1 `AND` e2) = applyMapping m e1 `AND` applyMapping m e2
applyMapping m (e1 `OR`  e2) = applyMapping m e1 `OR`  applyMapping m e2
applyMapping m (X i) =
    case M.lookup i m of
        Just b  -> Pure b
        _       -> X i

-- | Convenience wrapper
--
--   > isSatisfiable $ X 1 `AND` NOT (X 1)
--   > Nothing
--
--   > isSatisfiable $ X 1 `OR` NOT (X 1)
--   > Just [ True || !( True ) ]
--
isSatisfiable :: Expression -> Maybe Expression
isSatisfiable e = case satisfy M.empty e of
    (m, True)  -> Just $ applyMapping m e
    (_, False) -> Nothing

-- | Convenience wrapper
--
--   > isNegatable $ X 1 `AND` NOT (X 1)
--   > Just [ False && !( False ) ]
--
--   > isNegatable $ X 1 `OR` NOT (X 1)
--   > Nothing
--
isNegatable :: Expression -> Maybe Expression
isNegatable e = case negate M.empty e of
    (m, False) -> Just $ applyMapping m e
    (_, True)  -> Nothing