ersatz
A monad for expressing SAT or QSAT problems using observable sharing.
http://github.com/ekmett/ersatz
Version on this page:  0.5@rev:1 
LTS Haskell 22.39:  0.5@rev:1 
Stackage Nightly 20241102:  0.5@rev:2 
Latest on Hackage:  0.5@rev:2 
ersatz0.5@sha256:83ac3c0d6a1e256f9a8cb0bd829242b516885069a08dee63f6713f6b6e5ce455,9425
Module documentation for 0.5
Ersatz
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 differentiates Ersatz is the use of observable sharing in the API.
For instance to define a full adder:
full_adder :: Bit > Bit > Bit > (Bit, Bit)
full_adder a b cin = (s2, c1  c2)
where (s1,c1) = half_adder a b
(s2,c2) = half_adder s1 cin
half_adder :: Bit > Bit > (Bit, Bit)
half_adder a b = (a `xor` b, a && b)
as opposed to the following code in satchmo:
full_adder :: Boolean > Boolean > Boolean
> SAT ( Boolean, Boolean )
full_adder a b c = do
let s x y z = sum $ map fromEnum [x,y,z]
r < fun3 ( \ x y z > odd $ s x y z ) a b c
d < fun3 ( \ x y z > 1 < s x y z ) a b c
return ( r, d )
half_adder :: Boolean > Boolean
> SAT ( Boolean, Boolean )
half_adder a b = do
let s x y = sum $ map fromEnum [x,y]
r < fun2 ( \ x y > odd $ s x y ) a b
d < fun2 ( \ x y > 1 < s x y ) a b
return ( r, d )
This enables you to use the a much richer subset of Haskell than the purely monadic metalanguage, and it becomes much easier to see that the resulting encoding is correct.
To allocate fresh existentially or universally quantified variables or to assert that a Bit is true and add the attendant circuit with sharing to the current problem you use the SAT monad.
verify_currying :: (MonadQSAT s m) => m ()
verify_currying = do
(x::Bit, y::Bit, z::Bit) < forall_
assert $ ((x && y) ==> z) === (x ==> y ==> z)
We can then hand that off to a SAT solver, and get back an answer:
main = solveWith depqbf verify_currying >>= print
Support is offered for decoding various Haskell datatypes from the solution provided by the SAT solver.
Examples
Included are a couple of examples included with the distribution.
Neither are as fast as a dedicated solver for their respective
domains, but they showcase how you can solve real world problems
involving 10s or 100s of thousands of variables and constraints
with ersatz
.
sudoku
% time ersatzsudoku
Problem:
┌───────┬───────┬───────┐
│ 5 3 │ 7 │ │
│ 6 │ 1 9 5 │ │
│ 9 8 │ │ 6 │
├───────┼───────┼───────┤
│ 8 │ 6 │ 3 │
│ 4 │ 8 3 │ 1 │
│ 7 │ 2 │ 6 │
├───────┼───────┼───────┤
│ 6 │ │ 2 8 │
│ │ 4 1 9 │ 5 │
│ │ 8 │ 7 9 │
└───────┴───────┴───────┘
Solution:
┌───────┬───────┬───────┐
│ 5 3 4 │ 6 7 8 │ 9 1 2 │
│ 6 7 2 │ 1 9 5 │ 3 4 8 │
│ 1 9 8 │ 3 4 2 │ 5 6 7 │
├───────┼───────┼───────┤
│ 8 5 9 │ 7 6 1 │ 4 2 3 │
│ 4 2 6 │ 8 5 3 │ 7 9 1 │
│ 7 1 3 │ 9 2 4 │ 8 5 6 │
├───────┼───────┼───────┤
│ 9 6 1 │ 5 3 7 │ 2 8 4 │
│ 2 8 7 │ 4 1 9 │ 6 3 5 │
│ 3 4 5 │ 2 8 6 │ 1 7 9 │
└───────┴───────┴───────┘
ersatzsudoku 1,13s user 0,04s system 99% cpu 1,179 total
regexpgrid
This solves the regular crossword puzzle from the MIT mystery hunt.
% time ersatzregexpgrid
ersatzregexpgrid 2,45s user 0,05s system 99% cpu 2,502 total
Contact Information
Contributions and bug reports are welcome!
Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.
Edward Kmett
Changes
0.5 [2023.09.08]

The
forall
function inErsatz.Variable
has been renamed toforall_
, since a future version of GHC will make the use offorall
as an identifier an error. 
The types of
decode
andsolveWith
have been slightly less general:decode :: MonadPlus f => Solution > a > f (Decoded a) +decode :: Solution > a > Maybe (Decoded a) solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m > StateT s m a > m (Result, n (Decoded a)) +solveWith :: (Monad m, HasSAT s, Default s, Codec a) => Solver s m > StateT s m a > m (Result, Maybe (Decoded a))
That is, these functions now use
Maybe
instead of an arbitraryMonadPlus
. This change came about because: Practically all uses of
solveWith
in the wild are already pickingn
to beMaybe
, and  The behavior of
decode
andsolveWith
forMonadPlus
instances besidesMaybe
could produce surprising results, as this behavior was not well specified.
 Practically all uses of

Fix a bug in which
decode
could return inconsistent results with solution that underconstrain variables. For instance:do b < exists pure [b, not b]
Previously, this could decode to
[False, False]
(an invalid assignment).ersatz
now adopts the convention that unconstrained nonnegativeLiteral
s will always be assignedFalse
, and unconstrained negativeLiteral
s will always be assignedTrue
. This means that the example above would now decode to[False, True]
.
0.4.13 [2022.11.01]
 Make the examples compile with
mtl2.3.*
.  Add more documentation to the
Ersatz.Relation.*
modules, theVariable
class, and the data types inErsatz.Bits
.
0.4.12 [2022.08.11]
 Add
Equatable
andOrderable
instances for more base and containers types  Add solver support for
z3
0.4.11 [2022.05.18]
 Allow building with
mtl2.3.*
andtransformers0.6.*
.
0.4.10 [2021.11.16]
 Allow the test suite to build with recent GHCs.
 Drop support for pre8.0 versions of GHC.
0.4.9 [2021.02.17]
 Allow building with
lens5.*
.  Change to
buildtype: Simple
0.4.8 [2020.01.29]
 Add
MonadSAT
andMonadQSAT
 Achieve forward compatibility with GHC proposal 229.
0.4.7 [2019.06.01]
 Add
anyminisat
andtrySolvers
0.4.6 [2019.05.20]
 Add support for
cryptominisat5
0.4.5 [2019.05.02]
 Allow
ersatzregexpgrid
to build withbase4.13
(GHC 8.8).
0.4.4 [2018.08.13]
 Avoid the use of failable pattern matches in
do
notation to support building with GHC 8.6, which enablesMonadFailDesugaring
.
0.4.3 [2018.07.03]
 Make the test suite compile on GHC 8.6.
 Allow building with
containers0.6
.
0.4.2
 Add
Semigroup
instances forClause
andFormula
.  Generalize
regular
,regular_in_degree
,regular_out_degree
,max_in_degree
,min_in_degree
,max_out_degree
, andmin_out_degree
to work over heterogeneous relations.  Add
buildFrom
toErsatz.Relation.Data
.  Add
difference
,reflexive_closure
, andsymmetric_closure
toErsatz.Relation.Op
.  Add
anti_symmetric
andtotal
toErsatz.Relation.Prop
.
0.4.1
 Add a library dependency on the
doctests
test suite
0.4
 Performance improvements for CNF printing and parsing
 Add the
Ersatz.Counting
,Ersatz.Relation
,Ersatz.Relation.Data
,Ersatz.Relation.Prop
, andErsatz.Relation.Op
modules  Eliminate the
Or
constructor fromBit
towards using AIG  Fix error in the SAT encoding of the
choose
function  Revamp
Setup.hs
to usecabaldoctest
. This makes it build withCabal2.0
, and makes thedoctest
s work withcabal newbuild
and sandboxes.
0.3.1
 Removed the explicit
Safe
annotations. They can’t be maintained by mere mortals. Patches to mark packages upstream asTrustworthy
will be accepted as needed.
0.3
 Unified
Encoding
andDecoding
intoCodec
 Unified the
forall
andexists
implementations into a singleliterally
method inVariable
class.  Added
Orderable
type class and instances  Added
Ersatz.Bits.Bits
for variablesized bit arithmetic.  Renamed
Ersatz.Bits.half_adder
tohalfAdder
 Renamed
Ersatz.Bits.full_adder
tofullAdder
 Added new examples
 Dropped
blaze
package dependency in favor of newerbytestring
 Significantly shrank the number of “Trustworthy” modules
 Added various generic
V1
instances  Added
Equatable
instances forMap
andIntMap
 Added
Ersatz.BitChar
module for computing withChar
andString
 Wider version bounds for
transformers
andmtl
.
0.2.6.1
 Exported
Ersatz.Variable.GVariable
0.2.6
temporary 1.2
support
0.2.5.1
 Slightly faster builds due to dropping the need for
templatehaskell
.
0.2.5
 Support for GHC 7.8 and
lens
4.x
0.2.3
 SafeHaskell support
0.2.2
 Added examples to the documentation.
 Made the examples build as
ersatzsudoku
andersatzregexpgrid
.
0.2.1
 Added
examples/sudoku
, a sudoku solver.
0.2.0.1
 Fixed an overly conservative bound on
containers
.
0.2
 Converted to
Control.Lens
internally.  Added
Ersatz.Solver.DepQBF
 Added a bunch of example dimacs files
 The types now prevent one from applying a solver that does not support QSAT to a problem that requires it
 Added
examples/regexpgrid
, a program that solves the regular expression crossword  Made some optimizations to the formula generation.
regexpgrid
went from 71737 literals and 427725 clauses to 8618 literals and 172100 clauses and got much faster  Based
and
andor
inBoolean
onFoldable
; addedall
andany
0.1.0.2
 Added correct links to the source repository and issue tracker to the cabal project
0.1
 Repository Initialized