Skip to content

cemulate/polyomino-solver

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

54 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Polyomino Solver

Try it here.

Construct a collection of standard and/or completely custom polyominos, and an arbitrary region to fit them in, and this web app will find and display a valid tiling that places all of the polyominos in the region (if it exists).

Uses web-component-polyomino for building, manipulating, and displaying polyominos.

How it works

Algorithm X

Knuth's "Algorithm X" (implemented with "Dancing Links") is the best algorithm to handle this problem, by reducing it to an Exact Cover Problem. The details are explained by Knuth himself in his paper. I use dlxlib as an implementation of Dancing Links, courtesy of taylorgj.

Converstion to SAT

The other two solving methods are much less efficient, and were the solutions I first discovered.

It's known that for arbitrary grids and arbitrary sets of polyominos, the problem of deciding whether or not the polyominos can fit together on the grid is an NP-Complete problem. Being NP-Complete, we can convert a tiling problem into an instance of a Boolean Satisfiability Problem, for which efficient solvers exist.

Tiling problems can be converted to SAT by introducing a boolean variable for each configuration that each piece could possibly exist in, and then adding clauses that state that a piece must exist in exactly one configuration, and no configurations can overlap.

Javascript SAT Solver

The problem is converted to a CNF file (a common input format for SAT solvers). After that, boolean-sat is applied to solve the problem. This is Javascript SAT solver based on my forked repo of the original code written by Gregory Duck of at University of Singapore. This is probably the least efficient method. Since the SAT problem must be specified in CNF, even the input file can get very large very quickly.

Z3 Webassembly

This was born out of an attempt to make the preceding method faster. Here, we convert the problem to SMT format, and use the Webassembly build of Microsoft Research's Z3 Theorem Prover. Generally speaking, this is a tool that can check the satisfiability of first-order logic statements over arbitrary theories, but we only utilize it for the predicate logic subset.