This package explores encoding and solving various puzzles using Ersatz. Ersatz is a library for generating SAT problems with a high-level level encoding.
In particular this library explores the use of a new symbolic set selection
encoding named Select and the use of a total map type named SparseMap.
Select makes it easy to work symbolically with a choice from a set of possibilities without creating a new encoding of the enumerated type in Ersatz. This is particularly useful for run-time defined possibilities.
SparseMap supports the generalized Boolean typeclass and makes it easy to work with bit-maps (or more complex types than bit) over arbitrary keys.
These solutions use the minisat program to actually compute solutions
to the generated SAT problems. You'll need to install this tool. Below are
some examples of how to do this.
Homebrew (macOS)
$ brew install minisat
Debian Linux
$ apt install minisat
The recommended way to build this repository is using cabal-install and
GHC 8.4.2. Make sure you're using a recent version of cabal-install.
$ git clone https://github.com/glguy/5puzzle
$ cd 5puzzle
$ cabal new-build
$ cabal new-run ToolName
The repository can also be built using stack
$ git clone https://github.com/glguy/5puzzle
$ cd 5puzzle
$ stack setup
$ stack build
$ stack exec ToolName
-
Coin - Finds a way to use a balance scale to find one coin that doesn't match the others in a set.
-
Handshakes - Solves a puzzle where a couple goes to a party and everyone shakes hands when they arrive.
-
Cube - Solves a puzzle where 17 rectangular solids are placed within a 5x5 cube.
-
Pentomino - Solves placing arbitrary puzzle pieces on an arbitrary 2D board allowing for rotating and flipping pieces. The example problem places pentominos on a square board.
-
Domino - Solve the covering of an NxM grid with dominos where two opposing corners are removed
-
Einstein - Solves a classic logic puzzle.
-
RegExp - Solves regular expression crossword puzzles. This implementation features both an efficient implementation of regular expressions without backreferences, and an inefficient one with backreferences.
-
Nonogram - Solves nonogram puzzles by encoding the clues as regular expressions and treating them like regular expression crossword puzzles.
-
Sudoku - Solves arbitrary Sudoku puzzles.
-
Tough - Solves the One Tough Puzzle 3x3 jigsaw puzzle.
-
SetGame - Computes a way to arrange all 81 Set cards into 27 sets.
-
Queens - Solves the generalized Eight queens puzzle
-
Zhed - Solves an minimizes solutions to Zhed