satchmo-1.0: test/Cage.hs

import Prelude hiding ( not )

import Satchmo.Relation
import Satchmo.Code
import Satchmo.Boolean
import Satchmo.Counting
import Satchmo.Solve

import Data.List ( inits, tails )
import System.Environment

-- | command line arguments: r g n
-- program looks for a (r,g) cage:
-- r-regular graph with girth g on n nodes

main :: IO ()
main = do
    argv <- getArgs
    let [ r, g, n ] = map read argv
    Just a <- solve $ cage r g n
    putStrLn $ table a

type Graph = Relation Int Int

cage r g n = do
    a <- relation ((1,1),(n,n))
    monadic assert [ symmetric a ]
    monadic assert [ irreflexive a ]
    monadic assert [ regular r a ]
    girth_at_least g a
    return $ decode a

girth_at_least :: Int -> Graph -> SAT ()
girth_at_least k g = sequence_ $ do
    let ((lo,_),(hi,_)) = bounds g
    c <- [ 3 .. k-1 ]
    xs <- sublists c [lo .. hi]
    return $ assert_no_circle xs g
    
assert_no_circle xs g = 
    assert $ do 
        (x,y) <- zip xs $ rotate 1 xs
        return $ not $ g ! (x,y)
            
sublists :: Int -> [a] -> [[a]]
sublists 0 xs = return []
sublists k xs = do
    ( pre, this : post ) <- splits xs
    that <- sublists (k-1) $ pre ++ post
    return $ this : that

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

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