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

[ algorithms, bsd3, library, logic ] [ Propose Tags ]

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)

[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1, 0.1.0.1, 0.1.0.2, 0.2, 0.2.0.1, 0.2.4, 0.2.5, 0.2.5.1, 0.2.6, 0.2.6.1, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.4.3, 0.4.4, 0.4.5, 0.4.6, 0.4.7, 0.4.8, 0.4.9, 0.4.10, 0.4.11, 0.4.12, 0.4.13, 0.5
Change log CHANGELOG.md
Dependencies array (>=0.2 && <0.5), base (>=4 && <6), blaze-builder (>=0.3 && <0.4), blaze-textual (>=0.2 && <0.3), bytestring (>=0.9 && <0.12), containers (>=0.2.0.1 && <0.5), data-default (>=0.5 && <0.6), ghc-prim, lens (>=3.8 && <4.0), mtl (>=1.1 && <2.2), process (>=1.1 && <1.2), temporary (>=1.1 && <1.2), transformers (>=0.3 && <0.4), unordered-containers (>=0.2 && <0.3) [details]
License BSD-3-Clause
Copyright (c) 2010-2013 Edward Kmett, (c) 2013 Johan Kiviniemi
Author Edward A. Kmett, Johan Kiviniemi
Maintainer Edward A. Kmett <ekmett@gmail.com>
Category Logic, Algorithms
Home page http://github.com/ekmett/ersatz
Bug tracker http://github.com/ekmett/ersatz/issues
Source repo head: git clone git://github.com/ekmett/ersatz.git
Uploaded by EdwardKmett at 2013-03-16T05:26:32Z
Distributions LTSHaskell:0.5, Stackage:0.5
Reverse Dependencies 3 direct, 0 indirect [details]
Downloads 18416 total (51 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for ersatz-0.2

[back to package description]

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.

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