-- | Programm druckt aussagenlogische Formel, -- die das N-Damen-Problem modelliert. -- ghc --make Queens -- ./Queens 8 | minisat /dev/stdin /dev/stdout import Control.Monad ( forM) import System.Environment type CNF = [ Clause ] -- verknüpft mit UND type Clause = [ Literal ] -- verknüpft mit ODER type Literal = Int -- Bsp: -3 = neg x3, +4 = x4 pos n i j = n * i + j + 1 neg n i j = negate $ pos n i j in_jeder_zeile_höchstens_eine :: Int -> CNF in_jeder_zeile_höchstens_eine n = do i <- [ 0 .. n-1 ] j <- [ 0 .. n-1 ] k <- [ j + 1 .. n-1 ] return [ neg n i j, neg n i k ] main = do [ arg ] <- System.Environment.getArgs let n = read arg :: Int cls = -- in_jeder_zeile_wenigstens_eine n in_jeder_zeile_höchstens_eine n -- Spalten -- Diagonalen putStrLn $ unwords [ "cnf", show (n*n) , show ( length cls ) ] forM cls $ \ cl -> putStrLn $ unwords $ map show $ cl ++ [0] return ()