Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
The famous U2 bridge crossing puzzle: http://www.brainj.net/puzzle.php?id=u2
- data U2Member
- type SU2Member = SBV U2Member
- bono :: SU2Member
- edge :: SU2Member
- adam :: SU2Member
- larry :: SU2Member
- type Time = Word32
- type STime = SBV Time
- crossTime :: U2Member -> Time
- sCrossTime :: SU2Member -> STime
- data Location
- type SLocation = SBV Location
- here :: SLocation
- there :: SLocation
- data Status = Status {}
- start :: Status
- type Move a = State Status a
- peek :: (Status -> a) -> Move a
- whereIs :: SU2Member -> Move SLocation
- xferFlash :: Move ()
- xferPerson :: SU2Member -> Move ()
- bumpTime1 :: SU2Member -> Move ()
- bumpTime2 :: SU2Member -> SU2Member -> Move ()
- whenS :: SBool -> Move () -> Move ()
- move1 :: SU2Member -> Move ()
- move2 :: SU2Member -> SU2Member -> Move ()
- type Actions = [(SBool, SU2Member, SU2Member)]
- run :: Actions -> Move [Status]
- isValid :: Actions -> SBool
- solveN :: Int -> IO Bool
- solveU2 :: IO ()
Modeling the puzzle
U2 band members. We want to translate this to SMT-Lib as a data-type, and hence the deriving mechanism.
sCrossTime :: SU2Member -> STime Source
The symbolic variant.. The duplication is unfortunate.
Location of the flash
The status of the puzzle after each move
xferPerson :: SU2Member -> Move () Source
Transferring a person to the other side
bumpTime2 :: SU2Member -> SU2Member -> Move () Source
Increment the time, when two people cross together
Actions
type Actions = [(SBool, SU2Member, SU2Member)] Source
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
Recognizing valid solutions
isValid :: Actions -> SBool Source
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
Solving the puzzle
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.