Find an optimal 4-tuple which satisfies a boolean expression

(I have post a question with bounty for several days (Find a best 4-tuple which fulfils a variable boolean formula), but unfortunately got no answer yet. Here I simplify it to a smaller problem and hope could get some ideas...)

I have a big boolean formulae as follows:

$\quad (c_0 \leq c \wedge c \geq a_0+e_0 \vee e \geq c_0-b_0 \wedge e_0 \leq e) \wedge$

$\quad \quad c \leq d \wedge d-e \geq a_0 \wedge c-f \leq b_0 \wedge e \leq f \wedge$

$\quad \quad (d \leq d_0 \vee f \leq d_0-a_0) \wedge (d \leq b_0+f_0 \vee f \leq f_0)$

where $a_0, b_0, c_0, d_0, e_0, f_0$ are integer constants (including $-\infty$ and $+\infty$) as arguments, and $c, d, e, f$ are integer variables (including $-\infty$ and $+\infty$) to find.

I have already a function area to measure the dimension of 4 integers: $area(c,d,e,f) = |c-d| \times |e-f|$

So I am looking for an algorithm to find an optimal 4-tuple $(c,d,e,f)$ which makes the big formula TRUE and the $area(c,d,e,f)$ is greater or equal to the dimension of any other 4-tuple which also satisfies the formula.

In other word, find $\text{Max}(area(c,d,e,f))$ subjet to the big formula.

Could anyone help? Thank you very much!

-

This is not an answer, but it's how I would proceed. Your conditions on $c, d, e,$ and $f$ translate to the following in a less Boolean language:

$$d\leq \min(d_0,b_0+f_0)$$

$$f\leq \min(d_0-a_0,f_0)$$

$$\max(c_0,a_0+e_0)\leq c\leq \min(d,b_0+f)$$

$$\max(c_0-b_0, e_0)\leq e\leq \min(d-a_0,f)$$

With boundary conditions like this, you could try to parameterize the components of the boundary surface (some kind of hacked up prism) and use Lagrange multipliers to find the optimal values of your function. There are at least $8$ components to this surface, and quite possibly more depending on the values of your constants.

-