ghc-ersatz
A monad for expressing SAT or QSAT problems using observable sharing
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.
BSD-3-Clause