(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!