求解 SMT 问题时添加约束的顺序

Question

假设我有一个非常简单的 SMT 问题 - 一些自由变量和一些约束 С。我还有一个额外的约束 EC。当 C 和 EC 都满足时，我想更喜欢一个解决方案，如果这不可能，则回退到 C-only 解决方案。

在这种情况下我应该如何调用 check-sat？直觉告诉我是这样的：

(assert C)
(push)
(assert EC)
(check-sat)
<dance happy dance if it worked, or ...>
(pop)
(check-sat)

但我怀疑pop会擦除求解器挖掘的所有知识，而第二个check-sat会从头开始。

我可以试试

(assert C)
(check-sat)
(push)
(assert EC)
(check-sat)
<dance happy dance if it worked, or ...>
(pop)
(check-sat)

问题是 - 我能否确定最后一个 (check-sat) 将是空操作，因为已经使用相同的约束集调用了 check-sat？

Answer 1

你写：

But I suspect that pop will wipe all the knowledge solver has mined, and the second check-sat will start from scratch.

不一定。仅依赖于 C 的学习子句不需要在 pop() 处丢弃，尽管这样做总是安全的。这可能取决于求解器。

The question is - can I be sure than the last (check-sat) will be a no-op, because there already was a call to check-sat with the same constraint set?

我不希望 SMT 求解器记住之前的 check-sat 是可满足的，之前的模型甚至是导致 SAT 结论的之前的决策序列（在你断言之后并检查了其他东西）。尽管如此，最后一个 check-sat 应该比第一个检查便宜得多，因为学习的子句不需要生成两次。

专注于纯 SMT 求解器，一个选择是使用 API 而不是 SMT-LIB 接口，这样就可以在第一个 [=15= 之后简单地保存 SAT 模型] 并且在 pop().

之后不需要第三个 check-sat

您可能想要将您的问题编码为 MaxSMT 问题。

Definition 2.3.4. (Partial Weighted MaxSMT, Partial MaxSMT, Weighted MaxSMT). A Partial Weighted MaxSMT problem is a pair <φ_h, φ_s> where φ_h is the set of "hard" T-clauses, and φ_s is a collection of positive-weighted "soft" T-clauses of the form <C_i, w_i>, and the goal is to find the maximum-weight set of T-clauses ψ_s, ψ_s ⊆ φ_s, such that φ_h ∪ ψ_s is T-satisfiable [NO06, CFG+10, ABP+11b, CGSS13a].

A Partial MaxSMT problem is a Partial Weighted MaxSMT problem in which all "soft" T-clauses in φ_s have a unitary weight.

A Weighted MaxSMT problem is a Partial Weighted MaxSMT problem in which the set of "hard" T-clauses φ_h is empty.

[source, p. 40]

在这种情况下，您可以将 EC 断言为一个或多个 软条款。

假设EC是一个约束列表ec_1, ..., ec_k，有两种情况：

你想让所有ec_1, ..., ec_k同时满足；那么你会写：
```
(assert C)
(assert-soft EC)
(check-sat)
(get-model)
```

您希望同时满足EC的最大可能子集；那么你会写：

(assert c)
(assert-soft ec_1)
(assert-soft ...)
(assert-soft ec_k)
(check-sat)
(get-model)

MaxSMT 由像 Barcelogic, OptiMathSAT and Z3.

这样的 OMT 求解器支持

求解 SMT 问题时添加约束的顺序

Order of adding constraints when solving an SMT problem

smt