ersatz-0.4.13: ersatz.cabal
name: ersatz
version: 0.4.13
license: BSD3
license-file: LICENSE
author: Edward A. Kmett, Eric Mertens, Johan Kiviniemi
maintainer: Edward A. Kmett <ekmett@gmail.com>
copyright: © 2010-2015 Edward A. Kmett, © 2014-2015 Eric Mertens, © 2013 Johan Kiviniemi
stability: experimental
homepage: http://github.com/ekmett/ersatz
bug-reports: http://github.com/ekmett/ersatz/issues
category: Logic, Algorithms
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\" (<https://github.com/ekmett/ersatz/raw/master/notes/grid.pdf grid.pdf>) from the 2013 MIT mystery hunt.
.
> % time ersatz-regexp-grid
.
"SPOILER"
.
> ersatz-regexp-grid 2,45s user 0,05s system 99% cpu 2,502 total
build-type: Simple
cabal-version: >= 1.10
tested-with: GHC == 8.0.2
, GHC == 8.2.2
, GHC == 8.4.4
, GHC == 8.6.5
, GHC == 8.8.4
, GHC == 8.10.7
, GHC == 9.0.2
, GHC == 9.2.2
extra-source-files:
.gitignore
.hlint.yaml
AUTHORS.md
CHANGELOG.md
README.md
notes/SPOILER.html
notes/grid.pdf
notes/papers.md
data-files:
data/dimacs/bf/bf0432-007.cnf
data/dimacs/bf/bf1355-075.cnf
data/dimacs/bf/bf1355-638.cnf
data/dimacs/bf/bf2670-001.cnf
data/dimacs/bf/descr.html
data/dimacs/bf/ssa0432-003.cnf
data/dimacs/bf/ssa2670-130.cnf
data/dimacs/bf/ssa2670-141.cnf
data/dimacs/bf/ssa6288-047.cnf
data/dimacs/bf/ssa7552-038.cnf
data/dimacs/bf/ssa7552-158.cnf
data/dimacs/bf/ssa7552-159.cnf
data/dimacs/bf/ssa7552-160.cnf
data/dimacs/blocksworld/anomaly.cnf
data/dimacs/blocksworld/bw_large.a.cnf
data/dimacs/blocksworld/bw_large.b.cnf
data/dimacs/blocksworld/bw_large.c.cnf
data/dimacs/blocksworld/descr.html
data/dimacs/blocksworld/huge.cnf
data/dimacs/blocksworld/medium.cnf
data/dimacs/bmc/bmc-ibm-1.cnf
data/dimacs/bmc/bmc-ibm-2.cnf
data/dimacs/bmc/bmc-ibm-3.cnf
data/dimacs/bmc/bmc-ibm-4.cnf
data/dimacs/bmc/bmc-ibm-5.cnf
data/dimacs/bmc/bmc-ibm-7.cnf
data/dimacs/logistics/descr.html
data/dimacs/logistics/logistics.a.cnf
data/dimacs/logistics/logistics.b.cnf
data/dimacs/logistics/logistics.c.cnf
data/dimacs/logistics/logistics.d.cnf
data/dimacs/parity/descr
data/dimacs/parity/par16-1-c.cnf
data/dimacs/parity/par16-1.cnf
data/dimacs/parity/par16-2-c.cnf
data/dimacs/parity/par16-2.cnf
data/dimacs/parity/par16-3-c.cnf
data/dimacs/parity/par16-3.cnf
data/dimacs/parity/par16-4-c.cnf
data/dimacs/parity/par16-4.cnf
data/dimacs/parity/par16-5-c.cnf
data/dimacs/parity/par16-5.cnf
data/dimacs/parity/par8-1-c.cnf
data/dimacs/parity/par8-1.cnf
data/dimacs/parity/par8-2-c.cnf
data/dimacs/parity/par8-2.cnf
data/dimacs/parity/par8-3-c.cnf
data/dimacs/parity/par8-3.cnf
data/dimacs/parity/par8-4-c.cnf
data/dimacs/parity/par8-4.cnf
data/dimacs/parity/par8-5-c.cnf
data/dimacs/parity/par8-5.cnf
data/dimacs/phole/descr.html
data/dimacs/phole/hole6.cnf
data/dimacs/phole/hole7.cnf
data/dimacs/phole/hole8.cnf
source-repository head
type: git
location: git://github.com/ekmett/ersatz.git
flag examples
description: Build examples
default: True
manual: True
library
ghc-options: -Wall
hs-source-dirs: src
default-language: Haskell2010
build-depends:
array >= 0.2 && < 0.6,
base >= 4.9 && < 5,
bytestring >= 0.10.4.0 && < 0.12,
containers >= 0.2.0.1 && < 0.7,
data-default >= 0.5 && < 0.8,
lens >= 4 && < 6,
mtl >= 1.1 && < 2.4,
process >= 1.1 && < 1.7,
semigroups >= 0.16 && < 1,
streams >= 3.3 && < 4,
temporary >= 1.1 && < 1.4,
transformers >= 0.3 && < 0.7,
unordered-containers == 0.2.*,
attoparsec
exposed-modules:
Ersatz
Ersatz.Bit
Ersatz.Bits
Ersatz.BitChar
Ersatz.Codec
Ersatz.Equatable
Ersatz.Internal.Formula
Ersatz.Internal.Literal
Ersatz.Orderable
Ersatz.Problem
Ersatz.Solution
Ersatz.Solver
Ersatz.Solver.DepQBF
Ersatz.Solver.Minisat
Ersatz.Solver.Z3
Ersatz.Variable
Ersatz.Counting
Ersatz.Relation
other-modules:
Ersatz.Internal.Parser
Ersatz.Internal.StableName
Ersatz.Solver.Common
Ersatz.Relation.Data
Ersatz.Relation.Prop
Ersatz.Relation.Op
executable ersatz-regexp-grid
-- description: An example program that solves the regular expression crossword problem <http://www.coinheist.com/rubik/a_regular_crossword/> using Ersatz.
if flag(examples)
build-depends:
base < 5,
containers,
ersatz,
fail,
lens,
mtl,
parsec >= 3.1 && < 3.2,
semigroups
else
buildable: False
main-is: Main.hs
other-modules:
RegexpGrid.Problem
RegexpGrid.Regexp
RegexpGrid.Types
default-language: Haskell2010
ghc-options: -Wall
hs-source-dirs: examples/regexp-grid
executable ersatz-sudoku
-- description: An example program that solves a sudoku problem using Ersatz.
if flag(examples)
build-depends:
array,
base < 5,
ersatz,
mtl
else
buildable: False
default-language: Haskell2010
main-is: Main.hs
other-modules:
Sudoku.Cell
Sudoku.Problem
ghc-options: -Wall
hs-source-dirs: examples/sudoku
-- test-suite properties
-- type: exitcode-stdio-1.0
-- ghc-options: -Wall
-- default-language: Haskell2010
-- build-depends:
-- array,
-- base < 5,
-- containers,
-- data-reify >= 0.5 && < 0.7,
-- ersatz,
-- mtl,
-- transformers,
-- test-framework >= 0.2.4 && < 0.9,
-- test-framework-quickcheck >= 0.2.4 && < 0.4,
-- test-framework-hunit >= 0.2.4 && < 0.4,
-- QuickCheck >= 1.2.0.0 && < 2.6,
-- HUnit >= 1.2.2.1 && < 1.3
--
-- hs-source-dirs: tests
-- Main-is: properties.hs
test-suite speed
type: exitcode-stdio-1.0
main-is: Speed.hs
hs-source-dirs: tests
build-depends: base, ersatz
default-language: Haskell2010
test-suite moore
type: exitcode-stdio-1.0
main-is: Moore.hs
hs-source-dirs: tests
build-depends: base, array, ersatz
default-language: Haskell2010
test-suite z001
type: exitcode-stdio-1.0
main-is: Z001.hs
hs-source-dirs: tests
build-depends: base, ersatz
default-language: Haskell2010