ersatz

A monad for expressing SAT or QSAT problems using observable sharing. http://github.com/ekmett/ersatz

 Version on this page: 0.4.4 LTS Haskell 12.22: 0.4.4 Stackage Nightly 2018-12-12: 0.4.4 Latest on Hackage: 0.4.4

See all snapshots `ersatz` appears in

Maintained by

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 :: (MonadState s m, HasQSAT s) => 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

0.4.4 [2018.08.13]

• Avoid the use of failable pattern matches in `do`-notation to support building with GHC 8.6, which enables `MonadFailDesugaring`.

0.4.3 [2018.07.03]

• Make the test suite compile on GHC 8.6.
• Allow building with `containers-0.6`.

0.4.2

• Add `Semigroup` instances for `Clause` and `Formula`.
• Generalize `regular`, `regular_in_degree`, `regular_out_degree`, `max_in_degree`, `min_in_degree`, `max_out_degree`, and `min_out_degree` to work over heterogeneous relations.
• Add `buildFrom` to `Ersatz.Relation.Data`.
• Add `difference`, `reflexive_closure`, and `symmetric_closure` to `Ersatz.Relation.Op`.
• Add `anti_symmetric` and `total` to `Ersatz.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`, and `Ersatz.Relation.Op` modules
• Eliminate the `Or` constructor from `Bit` towards using AIG
• Fix error in the SAT encoding of the `choose` function
• Revamp `Setup.hs` to use `cabal-doctest`. This makes it build with `Cabal-2.0`, and makes the `doctest`s work with `cabal new-build` and sandboxes.

0.3.1

• Removed the explicit `Safe` annotations. They can’t be maintained by mere mortals. Patches to mark packages upstream as `Trustworthy` will be accepted as needed.

0.3

• Unified `Encoding` and `Decoding` into `Codec`
• Unified the `forall` and `exists` implementations into a single `literally` method in `Variable` class.
• Added `Orderable` type class and instances
• Added `Ersatz.Bits.Bits` for variable-sized bit arithmetic.
• Renamed `Ersatz.Bits.half_adder` to `halfAdder`
• Renamed `Ersatz.Bits.full_adder` to `fullAdder`
• Dropped `blaze` package dependency in favor of newer `bytestring`
• Significantly shrank the number of “Trustworthy” modules
• Added various generic `V1` instances
• Added `Equatable` instances for `Map` and `IntMap`
• Added `Ersatz.BitChar` module for computing with `Char` and `String`
• Wider version bounds for `transformers` and `mtl`.

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 `template-haskell`.

0.2.5

• Support for GHC 7.8 and `lens` 4.x

0.2.2

• Added examples to the documentation.
• Made the examples build as `ersatz-sudoku` and `ersatz-regexp-grid`.

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/regexp-grid`, a program that solves the regular expression crossword
• Made some optimizations to the formula generation. `regexp-grid` went from 71737 literals and 427725 clauses to 8618 literals and 172100 clauses and got much faster
• Based `and` and `or` in `Boolean` on `Foldable`; added `all` and `any`

0.1.0.2

• Added correct links to the source repository and issue tracker to the cabal project

0.1

• Repository Initialized
Depends on 15 packages:
Used by 3 packages: