# ersatz: A monad for expressing SAT or QSAT problems using observable sharing.

[ algorithms, bsd3, library, logic ] [ Propose Tags ]

A monad for expressing SAT or QSAT problems using observable sharing.

For example, we can express a full-adder with:

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)

Longer 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.

ersatz-sudoku
% time ersatz-sudoku
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 │
└───────┴───────┴───────┘
ersatz-sudoku  1,13s user 0,04s system 99% cpu 1,179 total
ersatz-regexp-grid

This solves the "regular crossword puzzle" (grid.pdf) from the 2013 MIT mystery hunt.

% time ersatz-regexp-grid

SPOILER

ersatz-regexp-grid  2,45s user 0,05s system 99% cpu 2,502 total

## Flags

### Manual Flags

NameDescriptionDefault
examples

Build examples

Enabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

#### Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

• No Candidates
Versions [RSS] 0.1, 0.1.0.1, 0.1.0.2, 0.2, 0.2.0.1, 0.2.4, 0.2.5, 0.2.5.1, 0.2.6, 0.2.6.1, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.4.3, 0.4.4, 0.4.5, 0.4.6, 0.4.7, 0.4.8, 0.4.9, 0.4.10, 0.4.11, 0.4.12, 0.4.13, 0.5 CHANGELOG.md array (>=0.2 && <0.6), attoparsec, base (>=4.9 && <5), bytestring (>=0.10.4.0 && <0.13), containers (>=0.2.0.1 && <0.8), data-default (>=0.5 && <0.8), ersatz, fail, lens (>=4 && <6), mtl (>=1.1 && <2.4), parsec (>=3.1 && <3.2), process (>=1.1 && <1.7), semigroups (>=0.16 && <1), streams (>=3.3 && <4), temporary (>=1.1 && <1.4), transformers (>=0.3 && <0.7), unordered-containers (>=0.2 && <0.3) [details] BSD-3-Clause © 2010-2015 Edward A. Kmett, © 2014-2015 Eric Mertens, © 2013 Johan Kiviniemi Edward A. Kmett, Eric Mertens, Johan Kiviniemi Edward A. Kmett Revision 1 made by ryanglscott at 2023-09-30T13:52:38Z Logic, Algorithms http://github.com/ekmett/ersatz http://github.com/ekmett/ersatz/issues head: git clone git://github.com/ekmett/ersatz.git by ryanglscott at 2023-09-18T10:26:28Z LTSHaskell:0.5, Stackage:0.5 3 direct, 0 indirect [details] ersatz-sudoku, ersatz-regexp-grid 18751 total (86 in the last 30 days) 2.0 (votes: 1) [estimated by Bayesian average] λ λ λ Docs uploaded by userBuild status unknown

[back to package description]

# 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

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 )

-> SAT ( Boolean, Boolean )
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 meta-language, 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 ersatz-sudoku
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 │
└───────┴───────┴───────┘
ersatz-sudoku  1,13s user 0,04s system 99% cpu 1,179 total


## regexp-grid

This solves the regular crossword puzzle from the MIT mystery hunt.

% time ersatz-regexp-grid

SPOILER

ersatz-regexp-grid 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