1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Puzzles.U2Bridge
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- The famous U2 bridge crossing puzzle: <http://www.braingle.com/brainteasers/515/u2.html>
-----------------------------------------------------------------------------
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}
module Documentation.SBV.Examples.Puzzles.U2Bridge where
import Control.Monad (unless)
import Control.Monad.State (State, runState, put, get, gets, modify, evalState)
import Data.List(sortOn)
import GHC.Generics (Generic)
import Data.SBV
-------------------------------------------------------------
-- * Modeling the puzzle
-------------------------------------------------------------
-- | U2 band members. We want to translate this to SMT-Lib as a data-type, and hence the
-- call to mkSymbolicEnumeration.
data U2Member = Bono | Edge | Adam | Larry
-- | Make 'U2Member' a symbolic value.
mkSymbolicEnumeration ''U2Member
-- | Model time using 32 bits
type Time = Word32
-- | Symbolic variant for time
type STime = SBV Time
-- | Crossing times for each member of the band
crossTime :: U2Member -> Time
crossTime Bono = 1
crossTime Edge = 2
crossTime Adam = 5
crossTime Larry = 10
-- | The symbolic variant.. The duplication is unfortunate.
sCrossTime :: SU2Member -> STime
sCrossTime m = ite (m .== sBono) (literal (crossTime Bono))
$ ite (m .== sEdge) (literal (crossTime Edge))
$ ite (m .== sAdam) (literal (crossTime Adam))
(literal (crossTime Larry)) -- Must be Larry
-- | Location of the flash
data Location = Here | There
-- | Make 'Location' a symbolic value.
mkSymbolicEnumeration ''Location
-- | The status of the puzzle after each move
--
-- This type is equipped with an automatically derived 'Mergeable' instance
-- because each field is 'Mergeable'. A 'Generic' instance must also be derived
-- for this to work, and the @DeriveAnyClass@ language extension must be
-- enabled. The derived 'Mergeable' instance simply walks down the structure
-- field by field and merges each one. An equivalent hand-written 'Mergeable'
-- instance is provided in a comment below.
data Status = Status { time :: STime -- ^ elapsed time
, flash :: SLocation -- ^ location of the flash
, lBono :: SLocation -- ^ location of Bono
, lEdge :: SLocation -- ^ location of Edge
, lAdam :: SLocation -- ^ location of Adam
, lLarry :: SLocation -- ^ location of Larry
} deriving (Generic, Mergeable)
-- The derived Mergeable instance is equivalent to the following:
--
-- instance Mergeable Status where
-- symbolicMerge f t s1 s2 = Status { time = symbolicMerge f t (time s1) (time s2)
-- , flash = symbolicMerge f t (flash s1) (flash s2)
-- , lBono = symbolicMerge f t (lBono s1) (lBono s2)
-- , lEdge = symbolicMerge f t (lEdge s1) (lEdge s2)
-- , lAdam = symbolicMerge f t (lAdam s1) (lAdam s2)
-- , lLarry = symbolicMerge f t (lLarry s1) (lLarry s2)
-- }
-- | Start configuration, time elapsed is 0 and everybody is here
start :: Status
start = Status { time = 0
, flash = sHere
, lBono = sHere
, lEdge = sHere
, lAdam = sHere
, lLarry = sHere
}
-- | A puzzle move is modeled as a state-transformer
type Move a = State Status a
-- | Mergeable instance for 'Move' simply pushes the merging the data after run of each branch
-- starting from the same state.
instance Mergeable a => Mergeable (Move a) where
symbolicMerge f t a b
= do s <- get
let (ar, s1) = runState a s
(br, s2) = runState b s
put $ symbolicMerge f t s1 s2
return $ symbolicMerge f t ar br
-- | Read the state via an accessor function
peek :: (Status -> a) -> Move a
peek = gets
-- | Given an arbitrary member, return his location
whereIs :: SU2Member -> Move SLocation
whereIs p = ite (p .== sBono) (peek lBono)
$ ite (p .== sEdge) (peek lEdge)
$ ite (p .== sAdam) (peek lAdam)
(peek lLarry)
-- | Transferring the flash to the other side
xferFlash :: Move ()
xferFlash = modify $ \s -> s{flash = ite (flash s .== sHere) sThere sHere}
-- | Transferring a person to the other side
xferPerson :: SU2Member -> Move ()
xferPerson p = do ~[lb, le, la, ll] <- mapM peek [lBono, lEdge, lAdam, lLarry]
let move l = ite (l .== sHere) sThere sHere
lb' = ite (p .== sBono) (move lb) lb
le' = ite (p .== sEdge) (move le) le
la' = ite (p .== sAdam) (move la) la
ll' = ite (p .== sLarry) (move ll) ll
modify $ \s -> s{lBono = lb', lEdge = le', lAdam = la', lLarry = ll'}
-- | Increment the time, when only one person crosses
bumpTime1 :: SU2Member -> Move ()
bumpTime1 p = modify $ \s -> s{time = time s + sCrossTime p}
-- | Increment the time, when two people cross together
bumpTime2 :: SU2Member -> SU2Member -> Move ()
bumpTime2 p1 p2 = modify $ \s -> s{time = time s + sCrossTime p1 `smax` sCrossTime p2}
-- | Symbolic version of 'Control.Monad.when'
whenS :: SBool -> Move () -> Move ()
whenS t a = ite t a (return ())
-- | Move one member, remembering to take the flash
move1 :: SU2Member -> Move ()
move1 p = do f <- peek flash
l <- whereIs p
-- only do the move if the person and the flash are at the same side
whenS (f .== l) $ do bumpTime1 p
xferFlash
xferPerson p
-- | Move two members, again with the flash
move2 :: SU2Member -> SU2Member -> Move ()
move2 p1 p2 = do f <- peek flash
l1 <- whereIs p1
l2 <- whereIs p2
-- only do the move if both people and the flash are at the same side
whenS (f .== l1 .&& f .== l2) $ do bumpTime2 p1 p2
xferFlash
xferPerson p1
xferPerson p2
-------------------------------------------------------------
-- * Actions
-------------------------------------------------------------
-- | A move action is a sequence of triples. The first component is symbolically
-- True if only one member crosses. (In this case the third element of the triple
-- is irrelevant.) If the first component is (symbolically) False, then both members
-- move together
type Actions = [(SBool, SU2Member, SU2Member)]
-- | Run a sequence of given actions.
run :: Actions -> Move [Status]
run = mapM step
where step (b, p1, p2) = ite b (move1 p1) (move2 p1 p2) >> get
-------------------------------------------------------------
-- * Recognizing valid solutions
-------------------------------------------------------------
-- | Check if a given sequence of actions is valid, i.e., they must all
-- cross the bridge according to the rules and in less than 17 seconds
isValid :: Actions -> SBool
isValid as = time end .<= 17 .&& sAll check as .&& zigZag (cycle [sThere, sHere]) (map flash states) .&& sAll (.== sThere) [lBono end, lEdge end, lAdam end, lLarry end]
where check (s, p1, p2) = (sNot s .=> p1 .> p2) -- for two person moves, ensure first person is "larger"
.&& (s .=> p2 .== sBono) -- for one person moves, ensure second person is always "bono"
states = evalState (run as) start
end = last states
zigZag reqs locs = sAnd $ zipWith (.==) locs reqs
-------------------------------------------------------------
-- * Solving the puzzle
-------------------------------------------------------------
-- | See if there is a solution that has precisely @n@ steps
solveN :: Int -> IO Bool
solveN n = do putStrLn $ "Checking for solutions with " ++ show n ++ " move" ++ plu n ++ "."
let genAct = do b <- free_
p1 <- free_
p2 <- free_
return (b, p1, p2)
res <- allSat $ isValid `fmap` mapM (const genAct) [1..n]
cnt <- displayModels (sortOn show) disp res
if cnt == 0 then return False
else do putStrLn $ "Found: " ++ show cnt ++ " solution" ++ plu cnt ++ " with " ++ show n ++ " move" ++ plu n ++ "."
return True
where plu v = if v == 1 then "" else "s"
disp :: Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()
disp i (_, ss)
| lss /= n = error $ "Expected " ++ show n ++ " results; got: " ++ show lss
| True = do putStrLn $ "Solution #" ++ show i ++ ": "
go False 0 ss
return ()
where lss = length ss
go _ t [] = putStrLn $ "Total time: " ++ show t
go l t ((True, a, _):rest) = do putStrLn $ sh2 t ++ shL l ++ show a
go (not l) (t + crossTime a) rest
go l t ((False, a, b):rest) = do putStrLn $ sh2 t ++ shL l ++ show a ++ ", " ++ show b
go (not l) (t + crossTime a `max` crossTime b) rest
sh2 t = let s = show t in if length s < 2 then ' ' : s else s
shL False = " --> "
shL True = " <-- "
-- | Solve the U2-bridge crossing puzzle, starting by testing solutions with
-- increasing number of steps, until we find one. We have:
--
-- >>> solveU2
-- Checking for solutions with 1 move.
-- Checking for solutions with 2 moves.
-- Checking for solutions with 3 moves.
-- Checking for solutions with 4 moves.
-- Checking for solutions with 5 moves.
-- Solution #1:
-- 0 --> Edge, Bono
-- 2 <-- Bono
-- 3 --> Larry, Adam
-- 13 <-- Edge
-- 15 --> Edge, Bono
-- Total time: 17
-- Solution #2:
-- 0 --> Edge, Bono
-- 2 <-- Edge
-- 4 --> Larry, Adam
-- 14 <-- Bono
-- 15 --> Edge, Bono
-- Total time: 17
-- Found: 2 solutions with 5 moves.
--
-- Finding all possible solutions to the puzzle.
solveU2 :: IO ()
solveU2 = go 1
where go i = do p <- solveN i
unless p $ go (i+1)
|
