ersatz

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

http://github.com/ekmett/ersatz

 Version on this page: 0.4.8 LTS Haskell 22.32: 0.5@rev:1 Stackage Nightly 2024-08-02: 0.5@rev:1 Latest on Hackage: 0.5@rev:1

See all snapshots ersatz appears in

Maintained by
This version can be pinned in stack with:ersatz-0.4.8@sha256:92ee1240dcc3d9ddbb67d321739b5901c5f3c56acd23b9671ca1c5ce0c86a32d,9266

Module documentation for 0.4.8

Depends on 16 packages(full list with versions):
Used by 1 package in lts-16.31(full list with versions):

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

0.4.8 [2020.01.29]

• Achieve forward compatibility with GHC proposal 229.

0.4.5 [2019.05.02]

• Allow ersatz-regexp-grid to build with base-4.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 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 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 doctests 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.
• 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.