Is it possible to find the optimal solution for a Boolean formula using SMT solvers?

Question

I have a big logical formula for the solution, due to the reason for editing, I need to insert the image here:

In addition, I already have an area function for measuring the dimension of 4 integers: area(c,d,e,f)=|c−d|×|e−f|

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

In other words, find the Max(area(c,d,e,f)) subtask of the large formula.

I am wondering if the SMT solver will help on this issue. I find out that Z3 supports quantifiers and can tell if a logical expression is feasible or not. But the question is whether Z3 can find the optimal solution for the area function.

Does anyone have any ideas? Any comments about SMT-solver, Z3 or other algorithms will be appreciated ...

Answer 1

In short, yes.

Since your formula is made up of quantifiers, I don't think the Microsoft Solver Foundation is the right choice. As you said, Z3 supports quantifiers, integer theory and is used to test feasibility. Although Z3 does not directly support optimization, you can easily code optimization tasks using universal quantifiers:

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

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

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

And on the side of the note, Z3 has a Linux distribution and provides an OCaml API that is fully suited to your preferences.

Answer 2

The objective function uses nonlinear integer arithmetic and quantifiers. Already non-linear integer arithmetic is tough (unsolvable) without quantifiers, and adding quantifiers makes it even worse. If you change the sorting from Int to Real, then we have a very limited quantifier exception for non-linear operations ((set-option: ELIM_QUANTIFIERS true) (set-option: ELIM_NLARITH_QUANTIFIERS true)) But this does not seem to be suitable for the problem you are, seems to decide. Try to understand whether it can be formulated as a problem with linear or quadratic optimization. There are many tools that are tuned for quadratic optimization (and they are perhaps less tuned, say, to boolean search that Z3). Try, for example, the Solver Foundation, which includes plugins for several optimization tools.

You can use Z3 to solve optimization problems, but a typical approach is to have a loop outside of Z3. First, you pose the problem that you want to test is doable, and then you search for the next satisfying job that improves the current one (which you are extracting from the satisfying model). To search for the next satisfying assignment, you will argue that "the target assigned to the next value you are looking for improves the" target "assigned to the current best value.

Below are some slides http://research.microsoft.com/en-us/people/nbjorner/lecture1.pptx this should be relevant. They are pretty close to solving this problem. The last slides in this deck show how to use the Z3s API to search through models. Of course, you can also use the text API if you want to write a parser for the output format. There are many more ways to interact with Z3 to optimize the problem, but they all require you to program an optimization search at the top of Z3. This can be useful when you have logical combinations of arithmetic restrictions and other areas supported by Z3, but standard optimization problems can be solved better using specialized optimization tools.

Answer 3

Your problem is not one of feasibility, but rather one of optimization problems or, in particular, mixed integer programming. This should not be difficult to solve with any solver, such as (since you checked your Z3 question and seem to be using Windows) Microsoft Solver Foundation , which also offers a free version.

Answer 4

I believe this page would be extremely useful. The example is well explained and this will help to read the whole article.