The problem is described in this Reddit post (web.archive.org).
The generator requires the size n x m of the area and returns a weighted partial MaxSAT formula.
A MaxSAT solver (not included) will provide the optimal solution for this formula as a variable assignment.
For sufficiently large areas (n > 2 and m > 2), the formula is always satisfiable.
The parser reads the output of the solver and produces a solution to the original problem.
A higher scoring solution of the MaxSAT formula corresponds to a higher scoring solution of the original problem, hence the (optimal) solution of the MaxSAT formula is the optimal solution of the original problem.
For an area of 5 x 12 use
python generate_wcnf.py | solve_maxsat | python parse_result.py
In place of solve_maxsat you need to call a MaxSAT solver that abides by the
DIMACS format of the Max-SAT 2016 evaluation.
One option that has worked flawlessly is Open-WBO.
More generally, e.g. for an area of 4 x 8, use
python generate_wcnf.py --width 4 --height 8 | solve_maxsat | python parse_result.py --width 4 --height 8
Alternatively, build and run a docker container that uses Open-WBO
solve_via_docker.sh 4 8
For an area of 5 x 12 on a Intel(R) Core(TM) i5-2500K CPU @ 3.30GHz system with 24 GB RAM running Open-WBO
it takes about 3:15 h (tested n=1 time).
For an area of 5 x 12 on a 13th Gen Intel® Core™ i5-13600KF × 20 system with 32 GB RAM running Open-WBO
it takes about 1:13 h (tested n=1 time).
For python generate_wcnf.py | solve_maxsat | python parse_result.py (an area of 5 x 12)
the output has been observed to be
An optimum solution was found.
T T W W W
T W W T W
W W T W W
W T W W T
T W W T W
W W T W W
W T W W T
W T W T T
W T W W T
W W T W W
T W W T W
T T W W W
Accordingly the optimal solution has a score of 234.