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