Question: How to use the SAT solver in maple to find a solution from a sat game?

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.

We can see that some graph problems such as the coloring problem and the problem of finding k-cliques can be transformed into SAT problem.  I am not familiar with how maple uses the sat solver. I am trying to use maple to solve the following game for a solution. The game is a good choice for understanding the SAT.

• http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php?level=1&lang=eng

The game is won when at least one cell on each line is green. 

Clicking on a number will color each cell with the same number in green, and each cell with the opposite number in red. 

For example:

If we choose ``1" as green(i.e. be chosen), then -1 is red (not be chosen) in any cell.  I guss that the maple function Satisfy can do it. 

That is, we are looking for a set of solutions such that at least one number in any line is selected as green. 

Here is a solution for winning this game:

How to use the SAT solver Satisfy in maple to find a solution from a sat game?