Coin flipping problem: Z3 and MaxSAT (Open-WBO)

Found this on reddit:

Coin flipping problem (KOI '06) (self.algorithms)

Hi. I'm struggling on this problem for weeks.

There is no official solution for this Korean Olympiad in Informatics problem.

The input is N × N coin boards, (0 < N < 33) 'H' means the coin's head is facing upward, and 'T' means the tail is facing upward.

The problem is minimizing T-coins with some operations:

    Flip all the coins in the same row.
    Flip all the coins in the same column.

Naïve O(N*2N) algorithm makes TLE. There are some heuristic approaches (Simulated Annealing) and branch-and-cut algorithm which reduces running time to about 200ms, but I have no idea to solve this problem in poly-time, or reduce this problem to any famous NP-complete problem.

Would you give some idea for me?

( )

My solution for Z3: see source code and comments, results.

And also MaxSAT solution (uses Open-WBO MaxSAT solver): source code, results. and are libraries which are used.

4-5 row/column flips can be achieved using this on 8*8 board (like chessboard) in reasonable time (couple of minutes).

All files:

→ [list of blog posts, my twitter/facebook]

Please drop me email about any bug(s) and suggestion(s): dennis(@)