Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Created February 1, 2012 04:26
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LeventErkok/1715097 to your computer and use it in GitHub Desktop.
Save LeventErkok/1715097 to your computer and use it in GitHub Desktop.
Hamiltonian Cycle detection using SBV
import Data.SBV
hamiltonian :: Int -> [(Integer, Integer)] -> IO (Maybe [Integer])
hamiltonian n edges = extractModel `fmap` satWith z3 hcycle
where isEdge p = bAny (.== p) [(literal x, literal y) | (x, y) <- edges]
validNodes xs = allDifferent xs &&& bAll (\x -> x .>= 0 &&& x .< fromIntegral n) xs
validEdges xs = bAll isEdge $ zip xs (tail xs ++ [head xs])
hcycle = do order <- mkFreeVars n
return $ validNodes order &&& validEdges order
-- Tests in ghci
-- *Main> hamiltonian 4 [(0,1), (1,2), (2,3), (3,0), (1,3)]
-- Just [3,0,1,2]
-- *Main> hamiltonian 4 [(0,1), (2,3), (3,0), (1,3)]
-- Nothing
@arey0pushpa
Copy link

sabbath@sabbath-Studio-XPS-1645:~/try_haskell$ ghci Hamiltonian.hs GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.

Hamiltonian.hs:1:8:
Could not find module `Data.SBV'
Perhaps you meant Data.Set (from containers-0.5.0.0)
Use -v to see a list of the files searched for.
Failed, modules loaded: none.

Tried few fixups :
sabbath@sabbath-Studio-XPS-1645:~/try_haskell$ ghci -XScopedTypeVariables

but shows :

Prelude> :m Data.SBV

:
Could not find module `Data.SBV'
Perhaps you meant Data.Set (from containers-0.5.0.0)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment