仅在优化方案中将断言软限制为可满足性？

Question

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

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

展示上述内容的示例：

(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

我的回答是是的，如果你逐步这样做。

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

然后，通过固定相关目标函数的值，很容易使可满足的软子句变得困难。尽管z3 不允许对软子句组的名称进行显式约束(AFAIK)，但可以通过使用lexicographic 多目标组合而不是@987654323 来隐式地做到这一点@一。

现在，在您的示例中，我们可以安全地从 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 问题，修复了软子句的布尔分配以使其变得困难，然后继续使用 pareto 组合优化多个目标。

---

请注意，如果 MaxSMT 问题允许多个相同权重的解决方案具有相同的最优值，那么之前的方法将丢弃它们并只关注一个分配。为了避免这种情况，理想的解决方案是固定 MaxSMT 目标的值，而不是固定其相关的布尔赋值，例如如下：

(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 组合并获得相同的结果。

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