satchmo-1.0: test/Ramsey.hs

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 ( inits, tails )
import Data.Ix
import qualified Data.Array as A
import Control.Monad ( forM, guard )
import System.Environment

-- | command line arguments: c_1 .. c_k n
-- program prints graph g that proves
-- R(c_1, .., c_k) > n

main :: IO ()
main = do
    argv <- fmap ( map read ) getArgs
    let cs = init argv
        n  = last argv
    Just a <- solve $ ramsey cs n
    print a

type Graph = Relation Int Int

ramsey cs n = do
    cols <- sequence $ replicate (length cs) $ do
        r <- relation ((1,1),(n,n))
        monadic assert [ symmetric r ]
        monadic assert [ irreflexive r ]
        return r
    circular_colouring ( n `div` length cs ) cols
    each_edge_is_coloured n cols
    forM ( zip cs cols ) no_monochromatic_clique
    return $ do
        ds <- mapM decode cols
        return $ do
            i <- range ((1,1),(n,n))
            let c = length $ takeWhile Prelude.not $ do d <- ds ; return $ d A.! i
            return ( i, c )

circular_colouring period cols = sequence_ $ do
    (col, col') <- zip cols $ rotate 1 cols
    x @ (p,q) <- indices col
    let y = (p+period,q+period)
    guard $ inRange ( bounds col ) y
    return $ do
        assert [ not $ col ! x, col' ! y ]

rotate :: Int -> [a] -> [a]
rotate k xs = 
    let ( pre, post ) = splitAt k xs
    in  post ++ pre

each_edge_is_coloured n cols = sequence_ $ do
    (p,q) <- range ((1,1),(n,n))
    guard $ p < q
    return $ assert $ do 
            col <- cols
            return $ col ! (p,q)

no_monochromatic_clique (c, col) = sequence_ $ do
    let ((lo,_),(hi,_)) = bounds col
    xs <- ordered_sublists c [lo .. hi]
    return $ assert $ do
        x : ys <- tails xs
        y <- ys
        return $ not $ col!(x,y)

ordered_sublists :: Int -> [a] -> [[a]]
ordered_sublists 0 xs = return []
ordered_sublists k xs = do
    ( pre, this : post ) <- splits xs
    that <- ordered_sublists (k-1) $ post
    return $ this : that

splits :: [a] -> [ ([a],[a]) ]
splits xs = zip ( inits xs ) ( tails xs )