Maximal saturated domino covering of a rectangle 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 &lt;= 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 =&gt; answer
1 2 =&gt; 1
1 3 =&gt; 2
1 9 =&gt; 6
1 10 =&gt; 6
2 2 =&gt; 2
2 3 =&gt; 4
2 5 =&gt; 7
3 3 =&gt; 6
3 4 =&gt; 8
3 7 =&gt; 15
4 4 =&gt; 12
4 7 =&gt; 21
Sagemath, 60 bytes
lambda m,n:m*n-len(graphs.GridGraph([m,n]).dominating_set())

Try it online!

From Saturated Domino Coverings by Buchanan et al:

Corollary 6.3: If \$B\$ is a rectangular \$m \times n\$ board, then \$d(B) = |B| - \gamma(G_{m,n})\$.

Where \$\gamma(\ldots)\$ is the domination number and \$G_{m,n}\$ is a grid graph. We also clearly have that if \$B\$ represents an \$m\times n\$ board then \$|B| = mn\$.