name: ersatz version: 0.5 x-revision: 2 license: BSD3 license-file: LICENSE author: Edward A. Kmett, Eric Mertens, Johan Kiviniemi maintainer: Edward A. Kmett 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\" () 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.7 , GHC == 9.4.5 , GHC == 9.6.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.13, containers >= 0.2.0.1 && < 0.8, data-default >= 0.5 && < 0.9, 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 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 hunit type: exitcode-stdio-1.0 main-is: HUnit.hs hs-source-dirs: tests build-depends: base, containers, data-default, ersatz, HUnit >= 1.2, test-framework >= 0.6, test-framework-hunit >= 0.2 default-language: Haskell2010 ghc-options: -Wall 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