• Python
• CNF SAT

Binairo is a sudoku-like game where the goal is to fill a grid with ones and zeros such that there are as much ones and zeros in every single row and column. Game grids start with already filled boxes, and some of them are unsolvable. Knowing which grids are solvable and which not is an NP-Complete problem for this reason the implemented program transforms a grid into a set of clauses (in CNF form) that is solved by a SAT solver.