Realisierung logischer Funktionen

module Satchmo.Boolean.Op where ...

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