Automatische Hilfsvariablen

im Quelltext: Haskell-Namen (x), für Solver: Nummern (1)

import Satchmo.Boolean 
import Satchmo.Solve
test :: IO ( Maybe Bool )
test = solve $ do 
    x <- boolean -- Allokation einer Variablen
    assert [ not x ]
    return $ decode x

Realisierung:

• boolean :: SAT Boolean (ist Aktion)
• automatisches Weiterzählen (StateMonad für Nummer)
• WriterMonad für CNF (Klauseln)
• ReaderMonad für Resultat (Belegung)