puzzle experiments and experimental puzzling
╭
𝟚𝟞·
Using summation for Slitherlink and Killer Sudoku is a natural choice, but Peano's Axioms are insufficient to define the integers using only first order logic. I want
┊
to dig into the theoretical concerns, but I'm going to defer them for now while I try to get some functionality working.
┊
┊
𝟚𝟝·
I'm a focused on solving logic pencil puzzles as Constraint Satisfaction Problems in part because I'd like to try my hand at a puzzle generator. Perhaps my ambition
┊
to share a monthly or even weekly sheet of puzzles at my local puzzle & game store is misguided, but for now it's on my hopes and dreams list.
┊
┊
𝟙𝟞·
To even solve the trivial Slitherlink Puzzle (a 1×1 puzzle with a single ‘4’) semi-symbolically, I'm going to have to up my constraint handling. My plan was to
┊
support constraint expressions - special objects which give some information about an otherwise indeterminate value.
┊
┊
My choice was to wrap a logical formula (another expression) using the variable ‘_’ to represent the constraint expression. This could get unweildy, so in practice I
┊
have kept them simple enough to be useful for my current, puzzle-solving purposes.
𝕁
┊
𝕒
┊
As an example, if x is ‘_∈{1 2}’ and y is ‘_∈{2 7}’ we can deduce ‘x+y’ will satisfy the constraint ‘_∈{3 4 8 9}’and we could also deduce from ‘x=y’ that ‘x=y=2’. The
𝕟
┊
pigeonholer I implemented to solve Sudoku puzzles in ⟪Silver⟫ starts with ‘_∈{1⋯9}’ for blank squares and 27 9-way not-equal expressions using an n-ary ‘¬=’ operator.
𝕦
┊
The handling is not Sudoku specific - I'm hoping it will work for a few more puzzles before I tidy things up.
𝕒
┊
𝕣
┊
Which brings me back to the start - I didn't implement constraint expressions properly, and now that I'm counting the number of edges around a square that are on the
𝕪
┊
path, I have to do at least some tidying.
┊
┊
𝟙𝟚·
puzzles The paper “Mathematical Definition and Systematization of Puzzle Rules” by Itsuki Maeda and Yasuhiro Inoue details a mathematical framework for logic pencil
┊
puzzles with formulas defining 10 different puzzle types. Nikoli, the company that popularized “Number Place” puzzles under the Japanese trademark ‘Sudoku’, publishes
┊
collections in Japan and describes each on their website:
┊
┊
┊
As I get my ⟪Silver⟫ Solver working on each, I'll post my ⟪Sapphire⟫ definitions.
┊
┊
𝟘𝟝·
I started on a formulation of Slitherlink rules in ⟪Sapphire⟫. Connectivity, as a pairwise relation could be easily satisfied by being true for any vertices that are
┊
connected to anything. I ended up defining a distance function with a special value (rather than a distinct relation) for ‘not connected’. In the next day or two,
╰
I'll see how ⟪Silver⟫ does trying to find a satisfying model (aka solution).
1
𝟮
𝟙𝟡·
Here's a link to the Sudoku rules I'm using for my experiments, written in my Sapphire logic syntax. So far, Sapphire supports first order formulae, integer
╰
operations and sets of integers. My ad-hoc "Silver Solver" supports partial evaluation and rewriting to try to find a satisfying model.
𝟵
/
𝟘𝟙·
Square Routes playtesting is just about happening!
