Inspired by this OEIS entry.
Background
A saturated domino covering is a placement of dominoes over an area such that
- the dominoes are completely inside the area,
- the dominoes entirely cover the given area,
- the dominoes may overlap, and
- removal of any domino reveals an uncovered cell (thus failing to satisfy condition 2).
The following is an example of a maximal such covering of 3 × 3
rectangle (since dominoes may overlap, each domino is drawn separately):
AA. B.. ..C ... ... ...
... B.. ..C .D. ... ...
... ... ... .D. EE. .FF
Challenge
Given the dimensions (width and height) of a rectangle, compute the maximum number of dominoes in its saturated domino covering.
You can assume the input is valid: the width and height are positive integers, and 1 × 1
will not be given as input.
Standard code-golf rules apply. The shortest code in bytes wins.
Test cases
A193764 gives the answers for square boards. The following test cases were verified with this Python + Z3 code (not supported on TIO).
Only the test cases for n <= m
are shown for brevity, but your code should not assume so; it should give the same answer for n
and m
swapped.
n m => answer
1 2 => 1
1 3 => 2
1 9 => 6
1 10 => 6
2 2 => 2
2 3 => 4
2 5 => 7
3 3 => 6
3 4 => 8
3 7 => 15
4 4 => 12
4 7 => 21