{{ message }}

Instantly share code, notes, and snippets.

# LeventErkok/RegexGridPuzzle.hs

Last active Mar 27, 2018
 {------------------------------------------------ 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 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 commented Aug 5, 2015

 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