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?

( https://www.reddit.com/r/algorithms/comments/7aq9if/coin_flipping_problem_koi_06/ )

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

And also MaxSAT solution (uses Open-WBO MaxSAT solver): source code, results. Xu.py and frolic.py 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: https://github.com/dennis714/yurichev.com/tree/master/blog/coin_flip.


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

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