ersatz-0.4.6: tests/Moore.hs

-- | graphs n nodes of degree <= d and diameter <= k 
-- see http://combinatoricswiki.org/wiki/The_Degree_Diameter_Problem_for_General_Graphs

-- usage: ./Moore d k n [s]
-- d : degree
-- k : diameter
-- n : nodes,
-- s : modulus for symmetry (see periodic_relation below)
-- s smaller => faster (more symmetries) but may lose solutions

-- test cases:  3 2 10 2  -- petersen graph
--              5 2 24    


{-# language FlexibleContexts #-}

import Prelude hiding ( not, or, and )
import qualified Prelude

import Ersatz
import Ersatz.Bit
import qualified Ersatz.Relation as R

import qualified Data.Array as A
import System.Environment (getArgs)
import Control.Monad ( void, when, forM )
import Control.Monad.State

main :: IO ( )
main = do
  argv <- getArgs
  case argv of
    [ d, k, n, s ] ->
      void $ mainf ( read d ) (read k) (read n) (read s)
    [ d, k, n    ] ->
      void $ mainf ( read d ) (read k) (read n) (read n)
    [] -> void $ mainf 3 2 10 5 -- petersen

mainf d k n s = do
  putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "symmetry ==", show s ]
  (s, mg) <- solveWith cryptominisat5 $ moore d k n s
  case (s, mg) of
     (Satisfied, Just g) -> do printA g ; return True
     _ -> do return False

moore :: (MonadState s m, HasSAT s )
      => Int -> Int -> Int -> Int
      -> m (R.Relation Int Int)
moore d k n s = do
  -- g <- R.symmetric_relation ((0,0),(n-1,n-1))
  g <- periodic_relation s ((0,0),(n-1,n-1))
  assert $ R.symmetric g
  assert $ R.reflexive g 
  assert $ R.max_in_degree (d+1) g 
  assert $ R.max_out_degree (d+1) g 
  let p = R.power k g
  assert $ R.complete p 
  return g

periodic_relation s bnd = do
  r <- R.relation bnd
  let normal (x,y) =
        if (x >= s Prelude.&& y >= s)
        then normal (x-s,y-s)  else (x,y)
  return $ R.build bnd $ do
    i <- A.range bnd
    return (i, r R.! normal i)
  
-- | FIXME: this needs to go into a library
printA :: A.Array (Int,Int) Bool -> IO ()
printA a = putStrLn $ unlines $ do
         let ((u,l),(o,r)) = A.bounds a
         x <- [u .. o]
         return $ unwords $ do 
             y <- [ l ..r ]
             return $ case a A.! (x,y) of
                  True -> "* " ; False -> ". "