As the documentation says: Ersatz is a library for generating QSAT (CNF/QBF) problems using a monad. It takes care of generating the normal form, encoding your problem, marshaling the data to an external solver, and parsing and interpreting the result into Haskell types.

Again, as the docs say: What differentiates Ersatz is the use of observable sharing in the API.

I would emphasize: *implicit* observable sharing. Because satchmo also has sharing, but in a very explicit way.

We want to construct a formula in propositional logic. A formula is a tree, but we want a DAG, to be able to share identical subtrees. This will reduce the cost of processing the formula (e.g., in the Tseitin transformation). - For example, assume we have pure functions

```
not :: Formula -> Formula
(&&) , (||) :: Formula -> Formula -> Formula
f a b = a && not b || not a && b
```

Then the expression "f (p && q) (r || s)" denotes a tree where each of the subtrees "(p && q), (r || s)" occurs twice.

If we run the Tseitin transformation on the formula, we process these occurences independently of each other, and build a fresh variable for each, while we would need just one.

Internally (in the Haskell run-time system), the tree it is quite likely represented as a DAG, where the occurences are shared, but there is no way to observe this sharing from the program.

This is what satchmo does: we leave the world of pure functions and expressions, and go to a state-like monad that produces DAG nodes. Then, "f (p && q) (r || s)" is translated to

`do { x <- p && q ; y <- r && s ; f x y }`

This solves the sharing problem, but forces to write ugly code.

Yes, but formula construction is pure. The monad is for these remaining reasons:

- allocating fresh variables ("exists")
- asserts ("assert")
- interface to external solver ("runSAT")

run this in ghci:

```
import Prelude hiding ( (&&), (||), not )
import qualified Prelude
import Ersatz
import Control.Monad
let f a b = a && not b || not a && b
runSAT' $ do [p,q,r,s]<- replicateM 4 exists ; assert $ f (p && q) (r || s) ; return [p,q,r,s::Bit]
```

output is

`([Var 2,Var 3,Var 4,Var 5],SAT 10 ((-10 | -9) & (-10 | 2) & (-10 | 3) & (-9 | 6) & (-9 | 8) & (-8 | -7) & (-8 | 4 | 5) & (-8 | 9 | 10) & (-7 | 2) & (-7 | 3) & (-7 | 6) & (-6 | 7 | 9) & (-5 | 8) & (-4 | 8) & (-3 | -2 | 7 | 8) & (-3 | -2 | 10) & (1) & (6)) mempty)`

This is 4 user-visible variables "[Var 2,Var 3,Var 4,Var 5]", and 10 back-end variables: 1 is always reserved for "constant True", then 4 user variables, and the remaining 5 are for the "&&" and "||" nodes in the DAG, where "not" does not need a node, since we can invert the literal. If you know the Tseitin transform, then you can check details.

we have to disambiguate the result types

```
( solveWith minisat $ do [p,q,r,s]<- replicateM 4 exists ; assert $ f (p && q) (r || s) ; return [p,q,r,s::Bit] ) :: IO ( Result, Maybe [Bool] )
```

with output

```
(Satisfied,Just [True,True,False,False])
```

Nothing, if you're just using the API.

Nothing, if you're adding another back-end that can handle CNFs. Does ersatz-toysat look easy enough?

For looking under the hood: start from here, where you'll find

```
data SAT = SAT
{ _lastAtom :: {-# UNPACK #-} !Int -- ^ The id of the last atom allocated
, _formula :: !Formula -- ^ a set of clauses to assert
, _stableMap :: !(HashMap (StableName ()) Literal) -- ^ a mapping used during 'Bit' expansion
} deriving Typeable
```

and then read up on weak pointers, stable names, etc.

Tseitin transform is in runBit. This uses generateLiteral and that's where the sharing actually is realized:

```
generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal
generateLiteral a f = do
let sn = unsafePerformIO (makeStableName' a)
use (stableMap.at sn) >>= \ ml -> case ml of
Just l -> return l
Nothing -> do
l <- literalExists
stableMap.at sn ?= l
f l
return l
```

Note that the contination "f" is only called if the name "sn" is not in the map.

Also, the snippet "use (stableMap.at sn) >>= ..." is typical lens speak.