optimization - 仅在优化场景中将断言软限制为可满足性可能吗？

Question

在优化任务中使用混合 assert 和 assert-soft 时，例如最大化，如果软断言会导致非最佳结果，则它们将被忽略。

是否可以将“软性”限制为仅可满足性搜索？即:如果软断言完全可以满足，那么它会被保留，然后在优化中被视为“硬”断言？

展示上述内容的示例:

(declare-fun x () Int)
(declare-fun y () Int)

(assert (< (+ x y) (* x y)))
(assert (>= x 0))
(assert (>= y x))
;(assert-soft (>= (* 4 x) y)); x->2, y->500
(assert (>= (* 4 x) y)); x->16, y->62
(assert (<= (* x y) 1000))

(maximize (+ x y))

(set-option :opt.priority pareto)
(check-sat)
(get-value (x y (+ x y) (* x y)))
(check-sat)
(get-value (x y (+ x y) (* x y)))
;...

这需要满足以下用例:

• 鉴于大量(>1000)变量(大多具有有限域)的复杂固定规则集，用户可以为其中任何变量选择所需的值，这可能会导致与规则集发生冲突。
• 变量的各个值都有评级/权重。

因此，给定一组用户选择的(可能有冲突的)选择、规则集本身以及最终所有可能选择集的评级，将找到所有变量的一个解决方案，在尊重用户所有非冲突选择的同时，最大化总评分。

我的想法是使用 assert-soft 进行用户选择，以消除冲突的选择，同时将其与 z3 的优化相结合以获得“最佳”解决方案。然而，这失败了，这就是这个问题的原因。

Answer 1

我的答案是是的，如果你逐步进行的话。

假设软子句集只有一个唯一 bool 赋值，这使得其关联的 MaxSMT 问题最优。

然后，通过固定相关目标函数的值，很容易使可满足的软子句变成硬子句。虽然z3不允许对软子句组的名称施加显式约束(据我所知)，可以通过使用 lexicographic 隐式地做到这一点多目标组合而不是 pareto一个。

现在，在您的示例中，我们可以安全地从 pareto 切换至lexicographic搜索，因为除了 assert-soft 隐式定义的目标函数之外，只有一个额外的目标函数。假设assert-soft的值群体被固定后，整个问题就会退化为一个单目标公式，而该公式又总是至多有一个帕累托最优解。

当然，如果计划在公式中添加更多目标，这是不可能的。在这种情况下，唯一的选择是增量式求解公式，如下所示:

(set-option:produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)

(declare-fun LABEL () Bool)
(assert (and 
    (or (not LABEL) (>= (* 4 x) y))
    (or LABEL (not (>= (* 4 x) y)))
)) ; ~= LABEL <-> (>= (* 4 x) y)
(assert-soft LABEL)

(assert (< (+ x y) (* x y)))
(assert (>= x 0))
(assert (>= y x))
(assert (>= (* 4 x) y))
(assert (<= (* x y) 1000))

(check-sat)
(get-model)
(push 1)
; assert LABEL or !LABEL depending on its value in the model

(maximize (+ x y))
; ... add other objective functions ...
(set-option :opt.priority pareto)
(check-sat)
(get-value (x y (+ x y) (* x y)))
(check-sat)
(get-value (x y (+ x y) (* x y)))
...
(pop 1)

这首先解决了 MaxSMT 问题，以一种使软子句变得困难的方式修复了软子句的 bool 赋值，然后继续使用 pareto 优化多个目标。组合。

<小时/>

请注意，如果 MaxSMT 问题对于相同的最优值承认多个相同权重的解决方案，则之前的方法将丢弃它们并仅关注一个分配。为了避免这种情况，理想的解决方案是固定 MaxSMT 目标的值，而不是固定其关联的 bool 赋值，例如如下所示:

(set-option:produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun LABEL () Bool)

(assert-soft (>= (* 4 x) y) :id soft)    

(assert (< (+ x y) (* x y)))
(assert (>= x 0))
(assert (>= y x))

(assert (>= (* 4 x) y))
(assert (<= (* x y) 1000))

(minimize soft)
(check-sat)
(get-model)
(push 1)
; assert `soft` equal to its value in model, e.g.:
; (assert (= soft XXX )))

(maximize (+ x y))
; ... add other objective functions ...
(set-option :opt.priority pareto)
(check-sat)
(get-value (x y (+ x y) (* x y)))
(check-sat)
(get-value (x y (+ x y) (* x y)))
...
(pop 1)

目前OptiMathSAT支持这种目标组合语法。仅有的。不幸的是，OptiMathSAT尚不支持非线性算术与优化结合使用，因此无法在您的示例中可靠地使用。

幸运的是，人们仍然可以使用这种方法 z3 !

如果除了一组软子句之外只有一个额外的目标函数，仍然可以使用 lexicographic组合而不是pareto一个并得到相同的结果。

否则，如果除了软子句组之外还有多个目标，则使用伪 bool 目标显式编码 MaxSMT 问题就足够了，而不是使用 assert-soft命令。通过这种方式，人们可以完全控制相关的目标函数，并且可以轻松地将其值固定为任何数字。但请注意，这可能会降低求解器处理公式的性能，具体取决于 MaxSMT 编码的质量。