Code in Python with PySat for Yashi Game

Bellow is the description of the project:

An instance of the Yashi game is specify by a n × n integer grid for some n > 2, on
which p > 2 nodes are placed. A solution of the game consists in drawing horizontal
and vertical segments, satisfying the following conditions:
1 No two segments cross each other.
2 The segments form a tree, i.e., they form a graph without cycles. Put differently
still, for every two nodes a and b there is exactly one path between a and b.
You can find out more about this game from the website
http://www.sumsumpuzzle.com/yashi.htm. Given an instance G of Yashi, develop a
SAT based method to answer the following questions
1 Decide if there is a solution for G. If
there is, return one solution.
2 Decide if there is a solution for G. If
there is, return the number of solutions.
3 Decide if there is a solution for G. If there
is, return a minimum-length solution.
Develop your own solution (preferred) or, alternatively, consider the SAT encoding
proposed in https://www.cs.bu.edu/faculty/kfoury/UNI-Teaching/CS512/AK_
Documents/Modeling-with-PL/main.pdf.