Explanation of the Ersatz Library

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")

Example, please?

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.

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.