Visualising and Modelling Puzzles - Demystify-rs

[ChrisJefferson]

demystify-rs is a Rust program for explaining pen and paper puzzles like Sudoku (what makes something a 'pen and paper' puzzle? You could print it out, and solve it with pen and paper :) )

It uses conjure (not conjure-oxide yet, but it will when conjure-oxide can refine all of conjure in the future), to translate puzzles to SAT, and then uses 'Minimal Unsatisfiable Sets' to solve those puzzles and (hopefully) explain how to solve them in a human-solvable way.

Demystify renders puzzles as SVGs (SVG is a format for drawing lines, circles, and text. It is commonly used on the internet). At the moment, there are 2 main issues

• The SVGs are not very good.
• There are a wide range of puzzles, with many different visual features. It would be good to implement as many as possible, and implement a generic framework for expressing puzzles.

I am happy to discuss this project, but the main objects I see are:

• Make a catalog of pen and paper puzzles
• Make a simple "visual language' to describe how to draw pen and paper puzzles.
• Extend the SVG output to render these puzzles, and explanations of these puzzles, well.

I do not expect the programming in this project to be highly difficult. It will require learning some basic SVG functionality.

I am happy to talk further about this project, and also give access to the repository for demystify-rs.

(Note, there is an earlier system, called 'demystify', written in Python. This has been replaced by a better, more general, Rust system).

To give you an idea of what demystify outputs look like, I attach to example outputs, but demystify implements about 14 puzzles types, and adding more is easy (but, they currently aren't drawn well! Also, they are very verbose...)
examples.zip

[ChrisJefferson]

Here is a sample image, just to show the kind of thing demystify current outputs (in this puzzle, binairo, each row and each column must contain three 0s (which should be 'black') and three 1s (which should be 'white'). As the row must be at least half black, then the last remaining cell which we can choose a value for must be 0.

[ChrisJefferson]

Here is another problem Star Battle, this is much more complicated deduction. In this problem we use 3 constraints:

1. There must be one thing which is '1' on row 2 (the '1' represents a star), there are two candidate spaces.

2. Stars cannot be adjacent, and the two squares in row 2 which could contain a star are both adjacent to (3,5)

So, (3,5) can't contain a star.