{-# language ScopedTypeVariables #-} import Prelude hiding ( not ) import qualified Prelude import Satchmo.Relation import Satchmo.Code import Satchmo.Boolean import Satchmo.Counting import Satchmo.Solve import Data.List (sort) import qualified Data.Array as A import Control.Monad ( guard, when ) import System.Environment -- | command line arguments: m n -- compute knight's tour on m x n chess board main :: IO () main = do argv <- getArgs let [ m, n ] = map read argv Just a <- solve \$ tour m n putStrLn \$ unlines \$ do let ((u,l),(o,r)) = A.bounds a x <- [u .. o] return \$ unwords \$ do y <- [ l ..r ] return \$ fill 4 \$ show \$ a A.! (x,y) fill k cs = replicate (k - length cs) ' ' ++ cs tour m n = do let s = m * n p :: Relation Int (Int,Int) <- bijection ((1,(1,1)), (s,(m,n))) sequence_ \$ do (i,j) <- zip [1..s] \$ rotate 1 [1..s] a <- A.range ((1,1),(m,n)) return \$ do assert \$ not ( p!(i,a)) : do b <- A.range ((1,1),(m,n)) guard \$ reaches a b return \$ p ! (j,b) assert \$ not ( p!(j,a)) : do b <- A.range ((1,1),(m,n)) guard \$ reaches a b return \$ p ! (i,b) return \$ do a <- decode p return \$ A.array ((1,1),(m,n)) \$ do ((i,p),True) <- A.assocs a return (p,i) bijection :: (A.Ix a, A.Ix b) => ((a,b),(a,b)) -> SAT ( Relation a b ) bijection bnd = do let ((u,l),(o,r)) = bnd a <- relation bnd sequence_ \$ do x <- A.range (u,o) return \$ monadic assert \$ return \$ exactly 1 \$ do y <- A.range (l,r) ; return \$ a!(x,y) sequence_ \$ do y <- A.range (l,r) return \$ monadic assert \$ return \$ exactly 1 \$ do x <- A.range (u,o) ; return \$ a!(x,y) return a reaches (px,py) (qx,qy) = 5 == (px - qx)^2 + (py - qy)^2 rotate :: Int -> [a] -> [a] rotate k xs = let ( pre, post ) = splitAt k xs in post ++ pre