1

I have a big boolean formula to solve, due to the reason of the redaction, I have to paste an image here:

enter image description here

Also, I have already a function area to measure the dimension of 4 integers: area(c,d,e,f)=|c−d|×|e−f|

I would like to do more than just figuring out if the formula is satisfiable: I am looking for an optimal 6-tuple (a,b,c,d,e,f) which makes the big formula TRUE and area(c,d,e,f) is greater or equal to the dimension of any other 6-tuple which also satisfies the formula.

In other word, find Max(area(c,d,e,f)) subjet to the big formula.

I am wondering if SMT solver could help on this problem. I learn that Z3 supports quantifiers, and be able to say if a boolean expression is satisfiable or not. But the question is if Z3 could help find the optimal solution for the function area.

Does anyone have any idea? Any comment about SMT solver, Z3 or other algorithms will appreciated...

Community
  • 1
  • 1
SoftTimur
  • 5,630
  • 38
  • 140
  • 292

4 Answers4

3

In short, yes.

Because your formula consists of quantifiers, I don't think Microsoft Solver Foundation is a suitable choice. As you said, Z3 supports quantifiers, theory of integers and is used for checking satisfiability. Although Z3 does not directly support optimization, you can easily encode optimization problems using universal quantifiers:

sat(a, b, c, d, e, f) => (forall a1, b1, c1, d1, e1, f1. sat(a1, b1, c1, d1, e1, f1) && goal(a, b, c, d, e, f) >= goal(a1, b1, c1, d1, e1, f1))

where: sat is your boolean expression for checking satisfiability and goal is the area function, your optimization goal.

As you can see, the formulation is literally translated from your requirement in the question. An assignment for (a, b, c, d, e, f) is the optimal solution you need to find.

And on a side note, Z3 has a Linux distribution and provides OCaml API, which totally fit your preference.

pad
  • 41,040
  • 7
  • 92
  • 166
  • Thanks for your comment, that is a good news... I havn't tried Z3 yet... My formula looks complicated, do you think Z3 can really handle this? – SoftTimur Dec 14 '11 at 21:50
  • Basically they are just integer constraints, boolean connectives and quantifiers. I'm sure that Z3 can handle it. – pad Dec 14 '11 at 21:54
  • Apparently this method costs a lot... I then have post another [question](http://stackoverflow.com/questions/8513809/how-to-optimize-a-piece-of-code-in-z3-pi-non-nested-arith-weight-related), if you are interested... Thanks – SoftTimur Dec 15 '11 at 00:57
3

The objective function uses non-linear integer arithmetic and quantifiers. Already non-linear integer arithmetic is tough (undecidable) without quantifiers, and adding quantifiers makes it even worse. If you change the sort from Int to Real, then we have very limited quantifier elimination for non-linear reals ((set-option :ELIM_QUANTIFIERS true) (set-option :ELIM_NLARITH_QUANTIFIERS true)) But this seems like not a real fit for the problem you seem to be solving. Try to see if it can be formulated as a linear or quadratic optimization problem. There are many tools that are tuned towards quadratic optimization (and they are perhaps less tuned towards, say the Boolean search that Z3 is). Try for instance the Solver Foundation which includes plugins for several optimization tools.

It is possible to use Z3 for solving optimization problems, but the typical approach is to have a loop outside of Z3. First you pose the problem you want to check is satisfiable, and then you search of a next satisfying assignment that improves the current one (that you retrieve from the satisfying model). To search for the next satisfying assignment you will assert that the ‘goal’ assigned to the next value you look for improves the ‘goal’ assigned to the current best value.

Here are some slides http://research.microsoft.com/en-us/people/nbjorner/lecture1.pptx that should be relevant. They come pretty close to dealing with this kind of problem. The last few slides in this deck illustrates how to use Z3’s API for searching through models. You can of course also use the text API if you like to write a parser for the output format. There are many more ways to interact with Z3 for optimization problems, but they all require you to program the optimization search on top of Z3. This can still be useful when you have Boolean combinations of constraints over arithmetic and other domains supported by Z3, but standard optimization problems can be solved better by dedicated optimization tools.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • I know it is an old question but I have the same problem and would like to check the slides you included in your answer but the link doesn't work. could you post it again? – Rehab11 May 14 '18 at 02:23
1

Your problem is not exactly one of satisfiability, but rather one of optimization or more specifically mixed integer programming. This shouldn't be too difficult to solve using any solver such as (since you tagged your question Z3 and you seem to be using Windows) Microsoft Solver Foundation, which also offers a free edition.

em70
  • 6,088
  • 6
  • 48
  • 80
  • Thanks for your comment... actually I am using Linux and code `Ocaml`. Now my concerns are if the Solver Foundation supports quantifier and has Ocaml API... – SoftTimur Dec 14 '11 at 15:10
1

I believe this page would be extremely useful. The example has been explained well, and it will help to read through the entire post.

dhrumeel
  • 574
  • 1
  • 6
  • 15