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.

Haskell Platform

$ 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