使用优化器最小化函数的图像

【问题标题】：Minimizing the Image of a function with an Optimizer使用优化器最小化函数的图像
【发布时间】：2018-02-18 17:46:40
【问题描述】：

是否可以使用优化器最小化函数的图像？如果没有，我还能如何实现它？

函数定义为 (declare-fun vmorph (V) V)

V 在哪里

(declare-datatypes () ((V V1 V2 V3 V4 V5 V6))).

还有其他规定使 vmorph 既不是满射也不是单射。我不想仅仅排除这两个，而是首先最小化 vmorph 的图像，理想情况下将所有元素映射到同一个元素。如果是 python，它会是这样的：

a = len({vmorph(v) for v in V})
minimize(a)

minimize 是我正在寻找的 z3 功能。

【问题讨论】：

恐怕你的问题没有任何上下文没有多大意义。您想要优化哪种类型的功能的哪个方面？这是否与 Z3 有任何关系，或者这是一个一般逻辑问题？

标签： z3 z3py

【解决方案1】：

也许您可以为每个V 分配一个“成本”函数并要求将其最小化。像这样的：

(declare-datatypes () ((V (V1) (V2) (V3) (V4) (V5) (V6))))

(declare-fun vmorph (V) V)

(define-fun cost ((x V)) Int (ite (= x V1) 1
                             (ite (= x V2) 2
                             (ite (= x V3) 3
                             (ite (= x V4) 4
                             (ite (= x V5) 5 6))))))

(minimize (+ (cost (vmorph V1))
             (cost (vmorph V2))
             (cost (vmorph V3))
             (cost (vmorph V4))
             (cost (vmorph V5))
             (cost (vmorph V6))))

(check-sat)
(get-model)

这将“偏爱”V1 而不是V2 而不是V3，等等。当然，这并不能保证为您提供全局最小值；因为所有人都喜欢V6 可能会更好。但是根据vmorph 的属性，您可能会想出一个很好的成本函数来达到您想要的效果。

【讨论】：