是否有可能找到一个布尔公式由SMT求解最优解？ [英] Is it possible to find optimal solution for a boolean formula by SMT solvers?

问题描述

我有一个很大的布尔公式来解决，因为新版本的原因，我要在这里贴上图片：

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

另外，我已经一个函数区域来衡量的4个整数尺寸：区（C，D，E，F）= | C-D |×| E-F |

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

我想不仅仅是搞清楚，如果公式是可满足做多：我在寻找一个最佳的6元组（A，B，C，D，E，F）这使得大公式 TRUE 和区（C，D，E，F）大于或等于任何其它6元组也满足式的尺寸

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.

在换句话说，找到 MAX（区（C，D，E，F）） subjet到大公式。

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

我想知道如果SMT求解器可以帮助这个问题。我知道 Z3 支持量词，并能够说，如果一个布尔EX pression是可满足与否。但问题是，如果 Z3 将有助于找到该函数的最优解区域。

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.

有没有人有什么想法？有关SMT解算器，Z3或其他算法，任何的评论将AP ​​preciated ...

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

推荐答案

总之，是的。

由于您的公式由量词，我不认为微软求解基金会是一个合适的选择。正如你所说，Z3支持量词，整数理论和用于检查可满足性。虽然Z3不直接支持的优化，你可以很容易地连接使用code优化问题全称量词：

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:

坐（A，B，C，D，E，F）=>（FORALL A1，B1，C1，D1，E1，F1坐（A1，B1，C1，D1，E1，F1）及。＆安培;   目标（A，B，C，D，E，F）> =目标（A1，B1，C1，D1，E1，F1））

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))

其中：坐在是布尔EX pression检查可满足性和目标是区域功能，你的优化目标。

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

正如你所看到的，配方是从字面上的问题，您的要求翻译。赋值为（A，B，C，D，E，F）是你需要找到最佳的解决方案。

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.

和在一个侧面说明，Z3有一个Linux发行版，并提供了OCaml的API，它完全适合你的preference。

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

这篇关于是否有可能找到一个布尔公式由SMT求解最优解？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！