Documentation.SBV.Examples.Puzzles.HexPuzzle

A solution to the hexagon solver puzzle: http://www5.cadence.com/2018ClubVQuiz_LP.html In case the above URL goes dead, here's an ASCII rendering of the problem.

We're given a board, with 19 hexagon cells. The cells are arranged as follows:

                    01  02  03
                  04  05  06  07
                08  09  10  11  12
                  13  14  15  16
                    17  18  19

• Each cell has a color, one of BLACK, BLUE, GREEN, or RED.
• At each step, you get to press one of the center buttons. That is, one of 5, 6, 9, 10, 11, 14, or 15.
• Pressing a button that is currently colored BLACK has no effect.
• Otherwise (i.e., if the pressed button is not BLACK), then colors rotate clockwise around that button. For instance if you press 15 when it is not colored BLACK, then 11 moves to 16, 16 moves to 19, 19 moves to 18, 18 moves to 14, 14 moves to 10, and 10 moves to 11.
• Note that by "move," we mean the colors move: We still refer to the buttons with the same number after a move.

You are given an initial board coloring, and a final one. Your goal is to find a minimal sequence of button presses that will turn the original board to the final one.

Documentation

data Color

Colors we're allowed

Constructors

Black

Blue

Green

Red

Instances

Eq Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

(==) :: Color -> Color -> Bool

(/=) :: Color -> Color -> Bool

Data Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Color -> c Color

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Color

toConstr :: Color -> Constr

dataTypeOf :: Color -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Color)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Color)

gmapT :: (forall b. Data b => b -> b) -> Color -> Color

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Color -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Color -> r

gmapQ :: (forall d. Data d => d -> u) -> Color -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Color -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Color -> m Color

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Color -> m Color

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Color -> m Color

Ord Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

compare :: Color -> Color -> Ordering

(<) :: Color -> Color -> Bool

(<=) :: Color -> Color -> Bool

(>) :: Color -> Color -> Bool

(>=) :: Color -> Color -> Bool

max :: Color -> Color -> Color

min :: Color -> Color -> Color

Read Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

readsPrec :: Int -> ReadS Color

readList :: ReadS [Color]

readPrec :: ReadPrec Color

readListPrec :: ReadPrec [Color]

Show Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

showsPrec :: Int -> Color -> ShowS

show :: Color -> String

showList :: [Color] -> ShowS

HasKind Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

kindOf :: Color -> Kind

hasSign :: Color -> Bool

intSizeOf :: Color -> Int

isBoolean :: Color -> Bool

isBounded :: Color -> Bool

isReal :: Color -> Bool

isFloat :: Color -> Bool

isDouble :: Color -> Bool

isRational :: Color -> Bool

isFP :: Color -> Bool

isUnbounded :: Color -> Bool

isUserSort :: Color -> Bool

isChar :: Color -> Bool

isString :: Color -> Bool

isList :: Color -> Bool

isSet :: Color -> Bool

isTuple :: Color -> Bool

isMaybe :: Color -> Bool

isEither :: Color -> Bool

showType :: Color -> String

SymVal Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Color)

literal :: Color -> SBV Color

fromCV :: CV -> Color

isConcretely :: SBV Color -> (Color -> Bool) -> Bool

forall :: MonadSymbolic m => String -> m (SBV Color)

forall_ :: MonadSymbolic m => m (SBV Color)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Color]

exists :: MonadSymbolic m => String -> m (SBV Color)

exists_ :: MonadSymbolic m => m (SBV Color)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Color]

free :: MonadSymbolic m => String -> m (SBV Color)

free_ :: MonadSymbolic m => m (SBV Color)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Color]

symbolic :: MonadSymbolic m => String -> m (SBV Color)

symbolics :: MonadSymbolic m => [String] -> m [SBV Color]

unliteral :: SBV Color -> Maybe Color

isConcrete :: SBV Color -> Bool

isSymbolic :: SBV Color -> Bool

SatModel Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

parseCVs :: [CV] -> Maybe (Color, [CV])

cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CV]) -> Maybe (b, [CV])

type SColor = SBV Color

Make Color a symbolic value.

sRed :: SBV Color

sGreen :: SBV Color

sBlue :: SBV Color

sBlack :: SBV Color

type Button = Word8

Use 8-bit words for button numbers, even though we only have 1 to 19.

type SButton = SBV Button

Symbolic version of button.

type Grid = SFunArray Button Color

The grid is an array mapping each button to its color.

next :: SButton -> Grid -> Grid

Given a button press, and the current grid, compute the next grid. If the button is "unpressable", i.e., if it is not one of the center buttons or it is currently colored black, we return the grid unchanged.

search :: [Color] -> [Color] -> IO ()

Iteratively search at increasing depths of button-presses to see if we can transform from the initial board position to a final board position.

example :: IO ()

A particular example run. We have:

>>> example
Searching at depth: 0
Searching at depth: 1
Searching at depth: 2
Searching at depth: 3
Searching at depth: 4
Searching at depth: 5
Searching at depth: 6
Found: [10,10,9,11,14,6]
Found: [10,10,11,9,14,6]
There are no more solutions.