Building a LinkedIn Tango Solver with Z3
A Z3 solver for LinkedIn's daily Tango puzzle: fill an n×n grid with suns and moons such that no three adjacent cells in any row or column share a symbol; row and column counts are balanced; and pairs of cells linked by = or × constraints match or oppose.
Each cell is a Boolean variable (True = sun). The adjacent-symbol rule is encoded by sliding a count over triples; balance is a simple sum-equals-half; equality and opposition constraints are direct Z3 clauses. Full solver code and a matplotlib visualisation are in the PDF.