ersatz
A monad for expressing SAT or QSAT problems using observable sharing.
http://github.com/ekmett/ersatz
LTS Haskell 22.43: | 0.5@rev:2 |
Stackage Nightly 2024-12-05: | 0.5@rev:2 |
Latest on Hackage: | 0.5@rev:2 |
ersatz-0.5@sha256:8ef8abed9dd9847344d6f8b1793ecf1f5dc24fe152095c6d093ca2a47b65a67c,9425
Module documentation for 0.5
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
(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 :: (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
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.5 [2023.09.08]
-
The
forall
function inErsatz.Variable
has been renamed toforall_
, since a future version of GHC will make the use offorall
as an identifier an error. -
The types of
decode
andsolveWith
have been slightly less general:-decode :: MonadPlus f => Solution -> a -> f (Decoded a) +decode :: Solution -> a -> Maybe (Decoded a) -solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a)) +solveWith :: (Monad m, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
That is, these functions now use
Maybe
instead of an arbitraryMonadPlus
. This change came about because:- Practically all uses of
solveWith
in the wild are already pickingn
to beMaybe
, and - The behavior of
decode
andsolveWith
forMonadPlus
instances besidesMaybe
could produce surprising results, as this behavior was not well specified.
- Practically all uses of
-
Fix a bug in which
decode
could return inconsistent results with solution that underconstrain variables. For instance:do b <- exists pure [b, not b]
Previously, this could decode to
[False, False]
(an invalid assignment).ersatz
now adopts the convention that unconstrained non-negativeLiteral
s will always be assignedFalse
, and unconstrained negativeLiteral
s will always be assignedTrue
. This means that the example above would now decode to[False, True]
.
0.4.13 [2022.11.01]
- Make the examples compile with
mtl-2.3.*
. - Add more documentation to the
Ersatz.Relation.*
modules, theVariable
class, and the data types inErsatz.Bits
.
0.4.12 [2022.08.11]
- Add
Equatable
andOrderable
instances for more base and containers types - Add solver support for
z3
0.4.11 [2022.05.18]
- Allow building with
mtl-2.3.*
andtransformers-0.6.*
.
0.4.10 [2021.11.16]
- Allow the test suite to build with recent GHCs.
- Drop support for pre-8.0 versions of GHC.
0.4.9 [2021.02.17]
- Allow building with
lens-5.*
. - Change to
build-type: Simple
0.4.8 [2020.01.29]
- Add
MonadSAT
andMonadQSAT
- Achieve forward compatibility with GHC proposal 229.
0.4.7 [2019.06.01]
- Add
anyminisat
andtrySolvers
0.4.6 [2019.05.20]
- Add support for
cryptominisat5
0.4.5 [2019.05.02]
- Allow
ersatz-regexp-grid
to build withbase-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 enablesMonadFailDesugaring
.
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 forClause
andFormula
. - Generalize
regular
,regular_in_degree
,regular_out_degree
,max_in_degree
,min_in_degree
,max_out_degree
, andmin_out_degree
to work over heterogeneous relations. - Add
buildFrom
toErsatz.Relation.Data
. - Add
difference
,reflexive_closure
, andsymmetric_closure
toErsatz.Relation.Op
. - Add
anti_symmetric
andtotal
toErsatz.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
, andErsatz.Relation.Op
modules - Eliminate the
Or
constructor fromBit
towards using AIG - Fix error in the SAT encoding of the
choose
function - Revamp
Setup.hs
to usecabal-doctest
. This makes it build withCabal-2.0
, and makes thedoctest
s work withcabal 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 asTrustworthy
will be accepted as needed.
0.3
- Unified
Encoding
andDecoding
intoCodec
- Unified the
forall
andexists
implementations into a singleliterally
method inVariable
class. - Added
Orderable
type class and instances - Added
Ersatz.Bits.Bits
for variable-sized bit arithmetic. - Renamed
Ersatz.Bits.half_adder
tohalfAdder
- Renamed
Ersatz.Bits.full_adder
tofullAdder
- Added new examples
- Dropped
blaze
package dependency in favor of newerbytestring
- Significantly shrank the number of “Trustworthy” modules
- Added various generic
V1
instances - Added
Equatable
instances forMap
andIntMap
- Added
Ersatz.BitChar
module for computing withChar
andString
- Wider version bounds for
transformers
andmtl
.
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
andersatz-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
andor
inBoolean
onFoldable
; addedall
andany
0.1.0.2
- Added correct links to the source repository and issue tracker to the cabal project
0.1
- Repository Initialized