Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Last active March 1, 2022 04:54
Show Gist options
  • Save LeventErkok/4942496 to your computer and use it in GitHub Desktop.
Save LeventErkok/4942496 to your computer and use it in GitHub Desktop.
{------------------------------------------------
A Haskell solution to: http://www.coinheist.com/rubik/a_regular_crossword/grid.pdf
using the Z3 SMT solver.
Z3 finds the following solution in about 7 mins
on my Mac Core-i5, and another 7 mins to prove
it's unique.
NHPEHAS
DIOMOMTH
FOXNXAXPH
MMOMMMMRHH
MCXNMMCRXEM
CMCCCCMMMMMM
HRXRCMIIIHXLS
OREOREOREORE
VCXCCHHMXCC
RRRRHHHRRU
NCXDXEXLE
RRDDMMMM
GCCHHCC
NB. This program uses the regex-genex package, make
sure you get the just released 0.6.0 version.
------------------------------------------------}
{-# LANGUAGE ImplicitParams #-}
import Regex.Genex
import Data.SBV
import Data.Char
mkChars :: Int -> Symbolic [SWord8]
mkChars n = do ns <- mkExistVars n
let a, z :: SWord8
a = literal (fromIntegral (ord 'A'))
z = literal (fromIntegral (ord 'Z'))
c i = constrain $ i .>= a &&& i .<= z
mapM_ c ns
return ns
puzzle :: Symbolic SBool
puzzle = do let ?maxRepeat = 13
let regexMN n = let ?maxRepeat = n in regexMatch
a@[a0, a1, a2, a3, a4, a5, a6] <- mkChars 7
b@[b0, b1, b2, b3, b4, b5, b6, b7] <- mkChars 8
c@[c0, c1, c2, c3, c4, c5, c6, c7, c8] <- mkChars 9
d@[d0, d1, d2, d3, d4, d5, d6, d7, d8, d9] <- mkChars 10
e@[e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10] <- mkChars 11
f@[f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11] <- mkChars 12
g@[g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12] <- mkChars 13
h@[h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11] <- mkChars 12
i@[i0, i1, i2, i3, i4, i5, i6, i7, i8, i9, i10] <- mkChars 11
j@[j0, j1, j2, j3, j4, j5, j6, j7, j8, j9] <- mkChars 10
k@[k0, k1, k2, k3, k4, k5, k6, k7, k8] <- mkChars 9
l@[l0, l1, l2, l3, l4, l5, l6, l7] <- mkChars 8
m@[m0, m1, m2, m3, m4, m5, m6] <- mkChars 7
constrain =<< regexMatch [".*H.*H.*"] a
constrain =<< regexMatch ["(DI|NS|TH|OM)*"] b
constrain =<< regexMatch ["F.*[AO].*[AO].*"] c
constrain =<< regexMatch ["(O|RHH|MM)*"] d
constrain =<< regexMatch [".*"] e
constrain =<< regexMatch ["C*MC(CCC|MM)*"] f
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMatch ["[^C]*[^R]*III.*"] g
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMN 5 ["(...?)\\1*"] h
constrain =<< regexMatch ["([^X]|XCC)*"] i
constrain =<< regexMatch ["(RR|HHH)*.?"] j
constrain =<< regexMatch ["N.*X.X.X.*E"] k
constrain =<< regexMatch ["R*D*M*"] l
constrain =<< regexMatch [".(C|HH)*"] m
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMatch [".*G.*V.*H.*"] [m0, l0, k0, j0, i0, h0, g0]
constrain =<< regexMatch ["[CR]*"] [m1, l1, k1, j1, i1, h1, g1, f0]
constrain =<< regexMatch [".*XEXM*"] [m2, l2, k2, j2, i2, h2, g2, f1, e0]
constrain =<< regexMatch [".*DD.*CCM.*"] [m3, l3, k3, j3, i3, h3, g3, f2, e1, d0]
constrain =<< regexMatch [".*XHCR.*X.*"] [m4, l4, k4, j4, i4, h4, g4, f3, e2, d1, c0]
constrain =<< regexMN 4 [".*(.)(.)(.)(.)\\4\\3\\2\\1.*"] [m5, l5, k5, j5, i5, h5, g5, f4, e3, d2, c1, b0]
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMatch [".*(IN|SE|HI)"] [m6, l6, k6, j6, i6, h6, g6, f5, e4, d3, c2, b1, a0]
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMatch ["[^C]*MMM[^C]*"] [ l7, k7, j7, i7, h7, g7, f6, e5, d4, c3, b2, a1]
constrain =<< regexMN 6 [".*(.)C\\1X\\1.*"] [ k8, j8, i8, h8, g8, f7, e6, d5, c4, b3, a2]
constrain =<< regexMatch ["[CEIMU]*OH[AEMOR]*"] [ j9, i9, h9, g9, f8, e7, d6, c5, b4, a3]
constrain =<< regexMatch ["(RX|[^R])*"] [ i10, h10, g10, f9, e8, d7, c6, b5, a4]
constrain =<< regexMatch ["[^M]*M[^M]*"] [ h11, g11, f10, e9, d8, c7, b6, a5]
constrain =<< regexMatch ["(S|MM|HHH)*"] [ g12, f11, e10, d9, c8, b7, a6]
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMatch [".*SE.*UE.*"] [ g12, h11, i10, j9, k8, l7, m6]
constrain =<< regexMatch [".*LR.*RL.*"] [ f11, g11, h10, i9, j8, k7, l6, m5]
constrain =<< regexMatch [".*OXR.*"] [ e10, f10, g10, h9, i8, j7, k6, l5, m4]
constrain =<< regexMatch ["([^EMC]|EM)*"] [ d9, e9, f9, g9, h8, i7, j6, k5, l4, m3]
constrain =<< regexMatch ["(HHX|[^HX])*"] [ c8, d8, e8, f8, g8, h7, i6, j5, k4, l3, m2]
constrain =<< regexMatch [".*PRR.*DDC.*"] [ b7, c7, d7, e7, f7, g7, h6, i5, j4, k3, l2, m1]
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMatch [".*"] [a6, b6, c6, d6, e6, f6, g6, h5, i4, j3, k2, l1, m0]
-------------------------------------------------------------------------------------------------------------------
constrain =<< regexMatch ["[AM]*CM(RC)*R?"] [a5, b5, c5, d5, e5, f5, g5, h4, i3, j2, k1, l0]
constrain =<< regexMatch ["([^MC]|MM|CC)*"] [a4, b4, c4, d4, e4, f4, g4, h3, i2, j1, k0]
constrain =<< regexMatch ["(E|CR|MN)*"] [a3, b3, c3, d3, e3, f3, g3, h2, i1, j0]
constrain =<< regexMN 4 ["P+(..)\\1.*"] [a2, b2, c2, d2, e2, f2, g2, h1, i0]
constrain =<< regexMatch ["[CHMNOR]*I[CHMNOR]*"] [a1, b1, c1, d1, e1, f1, g1, h0]
constrain =<< regexMatch ["(ND|ET|IN)[^X]*"] [a0, b0, c0, d0, e0, f0, g0]
return true
main :: IO ()
main = extractModel `fmap` satWith z3{timing=True} puzzle >>= display
where points = [7,8,9,10,11,12,13,12,11,10,9,8,7]
expected = sum points
mask c | isAscii c = c
| True = '_'
extract n xs = let (f, r) = splitAt n xs in (map (mask . chr . fromIntegral) f, r)
center s = replicate lp ' ' ++ s ++ replicate rp ' '
where e = 13 - length s
rp = e `div` 2
lp = e - rp
go [] [] = return ()
go (p:ps) xs
| p == length f = putStrLn (center f) >> go ps r
| True = error "Mismatched lengths"
where (f, r) = extract p xs
display :: Maybe ([Word8], [Word64]) -> IO ()
display Nothing = putStrLn "No solution."
display (Just (xs, _))
| length xs /= expected
= error $ "Expected " ++ show expected ++ " chars, got: " ++ show (length xs)
| True
= go points xs
@audreyt
Copy link

audreyt commented Feb 13, 2013

Awesome! Thank you for the pull requests, and regex-genex 0.6.0 has landed on Hackage with the required fixes.

@waltertross
Copy link

the link to the pdf is broken. Maybe this is more stable:
http://www.mit.edu/~puzzle/2013/coinheist.com/rubik/a_regular_crossword/grid.pdf

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment