satchmo-1.0: test/HC.hs

{-# 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