This repository contains a Z3-based tool for solving Tatamibari puzzles and, as an example set of puzzles, gadgets that prove the game NP-hard (from a forthcoming paper by the same authors, "Tatamibari is NP-complete").
tatamibari-solver.py solves Tatamibari puzzles
by reducing them to a satisfiability problem and solving them via
Z3.
It has the following prerequisites:
- Python 3.5+
- Z3
- Python Z3 wrapper
(
pip3 install z3-solver)
The NP-hardness gadgets are in the gadgets directory.
Within that directory, you can run make to solve the gadgets and
generate the figures of the paper.
In addition to the above prerequisites, you need the following software to visualize the output: