Beispiel SAT-Codierung

-- | 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 ()