Yashi-Game

SAT-based approach for solving the Yashi Game. Final project for the Knowledge Representation and Learning course at UniPd.

Game Rules:

An instance of the Yashi game is specified by a n x n integer grid, on which p nodes are placed.
A solution of the game consists in drawing horizontal and vertical segments, satisfying the following conditions:

• No two segments cross each other
• The segments form a tree (they form a graph without cycles)

Solutions:

Given an instance of the Yashi Game, some constraints are defined in order to determine if a solution exists. The PySAT library was used to define the formulas and to access the solvers.
A SAT solver (Minisat22) was used to identify a solution for the game, a MaxSAT solver (based on the Fu&Malik MaxSAT algorithm) was used to find the minimum-length solution.

.