# What is the purpose of the library?

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.

# What is so special about it?

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.

# Why do we want observable sharing?

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.

# How do we get explicit sharing?

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.

# But ersatz still is monadic?

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

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.

# Example for actually calling an external solver?

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])
``````

# What do I need to know about the implementation?

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.