ersatz

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

http://github.com/ekmett/ersatz

Version on this page:0.3.1
LTS Haskell 22.13:0.5@rev:1
Stackage Nightly 2024-03-14:0.5@rev:1
Latest on Hackage:0.5@rev:1

See all snapshots ersatz appears in

BSD-3-Clause licensed by Edward A. Kmett, Eric Mertens, Johan Kiviniemi
Maintained by Edward A. Kmett
This version can be pinned in stack with:ersatz-0.3.1@sha256:9e49180ea7c0db89d36e8c1580dd90e8bd83ef41883c073bcdb90646dda6985d,8668

Ersatz

Build Status

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

Changes

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
  • Added new examples
  • 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.3

  • SafeHaskell support

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