ersatz
Version 0.5 revision 2 uploaded by ryanglscott.
Package meta
- Synopsis
- A monad for expressing SAT or QSAT problems using observable sharing.
- Description
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
ersatz-regexp-grid 2,45s user 0,05s system 99% cpu 2,502 total
- Author
- Edward A. Kmett, Eric Mertens, Johan Kiviniemi
- Bug reports
- http://github.com/ekmett/ersatz/issues
- Category
- Logic, Algorithms
- Copyright
- © 2010-2015 Edward A. Kmett, © 2014-2015 Eric Mertens, © 2013 Johan Kiviniemi
- Homepage
- http://github.com/ekmett/ersatz
- Maintainer
- Edward A. Kmett <ekmett@gmail.com>
- Package URL
- n/a
- Stability
- experimental