Is it possible to find optimal solution for a bool

问题:

I have a big boolean formula to solve, due to the reason of the redaction, I have to paste an image 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...

回答1:

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.

回答2:

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.

回答3:

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.

回答4:

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