Realisierung logischer Funktionen

and :: [ Boolean ] -> SAT Boolean
and xs = do
  y <- boolean -- Hilfsvariable lt. Tseitin
  forM xs $ \ x -> do
      assert [ not y, x ]
  assert $ y : map not xs
  return y

Übung:

• Typ von forM (benutze :i forM in ghci oder http://haskell.org/hoogle/)
• or
• xor (Anzahl der True ist ungerade)