{-# LANGUAGE ScopedTypeVariables, CPP #-} {-# OPTIONS_GHC -Wall #-} module Main where import Control.Monad import Data.Array.IArray import System.Environment import qualified ToySolver.SAT as SAT import ToySolver.Internal.Util (setEncodingChar8) main :: IO () main = do #ifdef FORCE_CHAR8 setEncodingChar8 #endif [s] <- getArgs let n = read s ans <- solve n case ans of Nothing -> putStrLn "NO SOLUTION" Just m -> do forM_ [1..n] $ \i -> do putStrLn [if m ! (i,j) then 'Q' else '.' | j <- [1..n]] solve :: Int -> IO (Maybe (Array (Int,Int) Bool)) solve n = do solver <- SAT.newSolver (a :: Array (Int,Int) SAT.Var) <- liftM (array ((1,1),(n,n))) $ forM [(i,j) | i <- [1..n], j <- [1..n]] $ \(i,j) -> do x <- SAT.newVar solver return ((i,j),x) forM_ [1..n] $ \i -> do SAT.addExactly solver [a ! (i,j) | j <- [1..n]] 1 forM_ [1..n] $ \j -> do SAT.addExactly solver [a ! (i,j) | i <- [1..n]] 1 forM_ [1..n] $ \k -> do SAT.addAtMost solver [a ! (k+o,1+o) | o <- [0..(n-k)]] 1 forM_ [2..n] $ \k -> do SAT.addAtMost solver [a ! (1+o,k+o) | o <- [0..(n-k)]] 1 forM_ [1..n] $ \k -> do SAT.addAtMost solver [a ! (k-o,1+o) | o <- [0 .. k-1]] 1 forM_ [2..n] $ \k -> do SAT.addAtMost solver [a ! (k+o,n-o) | o <- [0..(n-k)]] 1 ret <- SAT.solve solver if ret then do m <- SAT.getModel solver return $ Just $ fmap (SAT.evalLit m) a else return Nothing