{- Constraint satisfaction solving |
|
Modifed from |
|
from http://www.haskell.org/haskellwiki/All_About_Monads#StateT_with_List |
|
-} |
|
import Data.Maybe |
import Control.Monad |
import Control.Monad.State |
import Text.Printf |
|
|
{- pretty printer for models, display using putStrLn |
Assumes that the list of variables in the assignments are ordered the |
same way for all assignments. |
-} |
|
showModels :: [Variables] -> String |
showModels models = |
if (length models) == 0 |
then |
"No solution exists!" |
else |
(concatMap fmtStr (namesOf (models !! 0))) |
++ "\n" ++ |
concatMap (++ "\n") ( |
map (concatMap fmtStr) (map valuesOf models) |
) |
where |
namesOf pairs = map fst pairs |
valuesOf pairs = map snd pairs |
fmtStr :: String -> String |
fmtStr s = printf "%8s" s |
|
{- |
A language to express logic problems |
|
Name are variables, named with strings |
Value are values of variables, values are strings |
VarType are the type of a variable, mapped to set of values |
Predicates are functions with values are true or false |
-} |
|
type Name = String |
type Value = String |
type VarType = String |
data Predicate = |
Is Name Value -- var has specific value |
| Equal Name Name -- vars have same (unspecified) value |
| And Predicate Predicate -- both are true |
| Or Predicate Predicate -- at least one is true |
| Not Predicate -- it is not true |
deriving (Eq, Show) |
|
type Variables = [(Name,Value)] |
|
-- derived predicates |
|
-- test for a variable NOT equaling a value |
isNot :: Name -> Value -> Predicate |
isNot var value = Not (Is var value) |
|
-- if a is true, then b must also be true |
implies :: Predicate -> Predicate -> Predicate |
implies a b = Not (a `And` (Not b)) |
|
-- iff |
iff :: Predicate -> Predicate -> Predicate |
iff a b = (a `implies` b) `And` (b `implies` a) |
|
-- exclusive or |
orElse :: Predicate -> Predicate -> Predicate |
orElse a b = (a `And` (Not b)) `Or` ((Not a) `And` b) |
|
{- |
Check a predicate with the given variable bindings. |
An unbound variable causes a Nothing return value. |
otherwise you get Just True or Just False. |
|
lookup takes a list of name-value tuples, and returns the |
corresponding value Just v, or Nothing if name is not present. |
|
lookup :: Eq a => a -> [(a, b)] -> Maybe b |
-} |
|
check :: Predicate -> Variables -> Maybe Bool |
check (Is var value) vars = do val <- lookup var vars |
return (val == value) |
check (Equal v1 v2) vars = do val1 <- lookup v1 vars |
val2 <- lookup v2 vars |
return (val1 == val2) |
|
{- |
lifting takes a function (a1 -> r) and turns it into a function |
on monads (m a1 -> m r) |
|
liftM :: Monad m => (a1 -> r) -> m a1 -> m r |
liftM2 :: Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m rSource |
|
Promote a function to a monad, scanning the monadic arguments from left |
to right. For example, |
|
liftM2 (+) [0,1] [0,2] = [0,2,1,3] |
liftM2 (+) (Just 1) Nothing = Nothing |
-} |
|
check (And p1 p2) vars = liftM2 (&&) (check p1 vars) (check p2 vars) |
check (Or p1 p2) vars = liftM2 (||) (check p1 vars) (check p2 vars) |
check (Not p) vars = liftM (not) (check p vars) |
|
{- |
Machinery for representing and solving constraint satisfaction problems. |
This is where we will define our combined monad. |
|
ProblemState is the type of our logic problem. Note the use of named |
fields where: |
vars is the environment, binding variables to values. |
constraints are a collection of predicates that must be satisfied |
in order for an environment to be a solution. |
-} |
|
data ProblemState = PS {vars::Variables, constraints::[Predicate]} |
|
-- this is our monad type for non-determinstic computations with state |
-- StateT is a ??? |
type NDS a = StateT ProblemState [] a |
|
-- lookup a variable in the environment. |
getVar :: Name -> NDS (Maybe Value) |
getVar v = do vs <- gets vars |
return $ lookup v vs |
|
-- set a variable in the environment. |
setVar :: Name -> Value -> NDS () |
setVar v x = do st <- get |
vs' <- return $ filter ((v/=).fst) (vars st) |
put $ st {vars=(v,x):vs'} |
|
{- |
Check if the variable assignments satisfy all of the predicates. |
The partial argument determines the value used when a predicate returns |
Nothing because some variable it uses is not set. Setting this to True |
allows us to accept partial solutions, then we can use a value of |
False at the end to signify that all solutions should be complete. |
|
Note: maybe :: b -> (a -> b) -> Maybe a -> b |
(maybe x id) (Just y) = y |
(maybe x id) Nothing = x |
is the way you yield a default value |
|
Note: (maybe x id) (Just y) = y |
(maybe x id) Nothing = x |
is the way you yield a default value |
-} |
|
isConsistent :: Bool -> NDS Bool |
isConsistent partial = do cs <- gets constraints |
vs <- gets vars |
let results = map (\p->check p vs) cs |
return $ and (map (maybe partial id) results) |
|
-- Return only the variable bindings that are complete consistent solutions. |
getFinalVars :: NDS Variables |
getFinalVars = do c <- isConsistent False |
guard c |
gets vars |
|
{- |
|
Get the first solution to the problem, by evaluating the solver computation |
with an initial problem state and then returning the first solution in the |
result list, or Nothing if there was no solution. |
|
-} |
|
getSolution :: NDS a -> ProblemState -> Maybe a |
getSolution c i = listToMaybe (evalStateT c i) |
|
-- Get a list of all possible solutions to the problem by evaluating the solver |
-- computation with an initial problem state. |
|
getAllSolutions :: NDS a -> ProblemState -> [a] |
getAllSolutions c i = evalStateT c i |
|
|
-- Test consistency over all allowed settings of the variable. |
|
tryAllValues :: (Name,VarType) -> NDS () |
tryAllValues (var,vtype) = do |
-- try all the possible values of the type of var using |
-- lookupType :: VarType -> [ Value ] |
-- note the use of monad sum to put plus between each possibility |
msum $ map (setVar var) (lookupType vtype) |
c <- isConsistent True |
guard c |
|
{- |
All that remains to be done is to define the puzzle in the predicate language |
and get a solution that satisfies all of the predicates: |
-} |
|
-- Define the problem, try all of the variable assignments and print a solution. |
|
{- |
solve takes a set of constraints and returns a list of all the variable |
assignments that satisfy the constraints. |
|
Each call to tryAllValues will fork the solution space, assigning the named |
variable to be "knight" in one fork and "knave" in the other. The forks which |
produce inconsistent variable assignments are eliminated (using the guard |
function). The call to getFinalVars applies guard again to eliminate |
inconsistent variable assignments and returns the remaining assignments as the |
value of the computation. |
|
if only asking for a few solutions, lazyness should stop further search |
|
-} |
|
solve :: [(Name,VarType)] -> [Predicate] -> [Variables] |
solve varOrder constraints = do |
let variables = [] |
problem = PS variables constraints |
|
(getAllSolutions |
(do |
sequence $ map tryAllValues varOrder |
getFinalVars) |
problem) |
|
pSolve :: [Predicate] -> IO () |
pSolve constraints = putStrLn (showModels $ solve varOrder constraints) |
|
{- |
|
We introduce types for the variables using a function lookupType that |
for each type gives the possible values it can have. |
|
The we identify the variables in the problem and their types, along with |
the order in which they should be searched, with the earliest variables |
being the most frequently changed (in model checking the order in which |
variables are examined can dramatically affect solution time). |
|
-} |
|
lookupType :: VarType -> [ Value ] |
varOrder :: [ (Name, VarType) ] |
|
{- Here is where the problem-specific definitions occur. -} |
|
-- a generic person |
lookupType "Per" = ["knight", "knave", "normal" ] |
-- just knights and knaves |
lookupType "KK" = ["knight", "knave" ] |
-- paths are good or bad |
lookupType "Path" = ["good", "bad" ] |
|
varOrder = [ |
("B", "KK"), |
("A", "KK"), |
("R", "Path"), |
("L", "Path") |
] |
|
said :: Name -> Predicate -> Predicate |
said v p = ((v `Is` "knight") `implies` p) `And` |
((v `Is` "knave") `implies` (Not p)) `And` |
((v `Is` "normal") `implies` (p `Or` (Not p))) |
|
-- lying is saying something is true when it isn't, or not saying anything |
lied :: Name -> Predicate -> Predicate |
lied v p = (v `said` p) `And` (Not p) |
|
-- telling truth is saying something is true when it is, or not saying anything. |
toldTruth :: Name -> Predicate -> Predicate |
toldTruth v p = (v `said` p) `implies` p |