nqueens.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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