0
$\begingroup$

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.

  • 0
    This looks sort of like a quadratic programming problem. You might want to look up "Quadratic Programming" on Wikipedia.2011-11-04

1 Answers 1

1

Have your find() function first generate a SAT instance that is satisfiable only if the original formula is satisfied. (Convert the formula to a circuit and then use Tseitin transformations to get to CNF.) Then add the constraint that the area() function must produce a value greater than some reasonable starting value N, say 1000. Run a SAT solver (e.g. Minisat) on the result. If the solver finds a solution, increase N and repeat. If the solver reports "unsatisfiable" decrease N and repeat, gradually bracketing N via binary search until you find the largest N that yields a satisfiable SAT instance. Extract the z variables encoded in the SAT solution and return them.