Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
The formula you give as an example isn't of the general form that it's supposed to be an example of -- it contains the arithmetic operator $+$. Please clarify exactly what sort of formulas you have in mind. You're stating the problem with a lot of generality -- if in fact you only have linear inequalities combined using logical connectives, then the problem might be rather straightforward. –  joriki Nov 1 '11 at 22:32
@joriki, thanks for your comment, you are right, i forgot to mention something important... I have updated my initial post... –  SoftTimur Nov 1 '11 at 23:40
This looks sort of like a quadratic programming problem. You might want to look up "Quadratic Programming" on Wikipedia. –  Craig Nov 4 '11 at 12:43
add comment

1 Answer

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.

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.