SAT-based approach for solving the Yashi Game. Final project for the Knowledge Representation and Learning course at UniPd.
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)
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.
.
