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