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

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.5@sha256:8ef8abed9dd9847344d6f8b1793ecf1f5dc24fe152095c6d093ca2a47b65a67c,9425

Ersatz

Hackage 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 :: (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

Changes

0.5 [2023.09.08]

  • The forall function in Ersatz.Variable has been renamed to forall_, since a future version of GHC will make the use of forall as an identifier an error.

  • The types of decode and solveWith 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 arbitrary MonadPlus. This change came about because:

    1. Practically all uses of solveWith in the wild are already picking n to be Maybe, and
    2. The behavior of decode and solveWith for MonadPlus instances besides Maybe could produce surprising results, as this behavior was not well specified.
  • 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-negative Literals will always be assigned False, and unconstrained negative Literals will always be assigned True. 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, the Variable class, and the data types in Ersatz.Bits.

0.4.12 [2022.08.11]

  • Add Equatable and Orderable instances for more base and containers types
  • Add solver support for z3

0.4.11 [2022.05.18]

  • Allow building with mtl-2.3.* and transformers-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 and MonadQSAT
  • Achieve forward compatibility with GHC proposal 229.

0.4.7 [2019.06.01]

  • Add anyminisat and trySolvers

0.4.6 [2019.05.20]

  • Add support for cryptominisat5

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 buildFrom to Ersatz.Relation.Data.
  • 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.
  • 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