jbosboom / tatamibari-solver

Z3-based Tatamibari solver, and figures from Tatamibari NP-hardness paper

Tatamibari solver and NP-hardness gadgets

Aviv Adler, Jeffrey Bosboom, Erik D. Demaine, Martin L. Demaine, Quanquan C. Liu, Jayson Lynch

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

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)

NP-hardness gadgets

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:

• svgtiler