在Z3中如何“最小化”工作

-2

我在Z3中使用最小化函数很多，我担心一些可伸缩性问题（当我最小化变量的数量增长时）。 “最小化”的底层算法是什么？有没有一种通用的方法来加快速度？在Z3中如何“最小化”工作

2017-08-25 Halaby

有关Z3中使用的优化算法的详细信息，请参阅此paper。关于你关于“加快速度的一般方法”的问题：“无法确切地知道你想要做什么以及你如何编码它。发表一个事例不“缩放”的具体例子可能会有所帮助。

2017-08-25 21:52:38

我的问题设置很简单：我正在努力满足多值逻辑子句C_1，...，C_m的最大数量。我使用位向量。 C_1或B_1 C_2或B_2 ... C_M或B_M 和我最小化b_i的：对于每个子句C_I，我用新鲜的变量（位向量）b_i间断它（最小化B_1）（最小化b_2）...（最小化b_m）所以我的问题是关于如何最小化位向量的工作原理以及是否有技巧来加速它。 – Halaby

听起来像你正在解决max-sat？如果是这样的话，软约束是顺其自然的方法：http://rise4fun.com/Z3/tutorialcontent/optimization#h23这个想法是，Z3尽力满足尽可能多的软约束，同时尝试将相关的惩罚保持在它不能满足的最低水平。 –

我正在解决MaxSAT，是的，但在多值逻辑。问题是（在我的理解）assert-soft接受布尔约束，我正在处理多值约束。 – Halaby

在Z3中如何“最小化”工作

回答

相关问题