I am looking for an algorithm...
I have a kind of boolean formulae which contain $\wedge$, $\vee$, $+$ as arithmetic operator, relational operators ($<, >, \ldots)$, 4 integer constants $c_0, \ldots, c_3$ (which could include infinity), a integer variable $i$, and another 4 integer constants $z_0, \ldots, z_3$ (which could include infinity).
The formulae have a limited form: the 2 operands of a relational operator could only be in the form: either a constant or $i$ + a constant. For instance, the formulae support $z_1 \leq c_0$ and $z_3 > i + z_1$, but do not support $z_0 + z_1 + z_2 > i$ (where the left operand have 3 components) or $z_2 > i + i$ (where the right operand have 2 i)...
Here is a more complicated formula of this kind:
$$(z_1 \geq c_1 \vee z_1 \geq i + c_3) \wedge (z_1 \geq z_0 \wedge z_1 \geq i + z_2) \wedge (i+z_3 \geq c_1 \vee i+z_3 \geq i + c_3)\ldots$$
I have already a function
area to measure the dimension of 4 constants: $area(z_0, z_1, z_2, z_3) = |z_1 - z_0| \times |z_3 - z_2|$.
I have 1 big major formula of this kind. I would like to find an algorithm
find, which takes 6 integer arguments: $a, b, c_0, \ldots c_3$, and finds 4 integers: $z_0, \ldots,z_3$, such that $\forall i, i \in [a, b]$ the formula is
true, and $area(z_0, z_1, z_2, z_3)$ could be as large as possible. The formula can be hard coded inside the algorithm, instead of being an argument.
Does anyone have a good idea?
Edit1: I have simplified the problem to a smaller one and post another thread: Find an optimal 4-tuple which satisfies a boolean expression.