z3 - 将 Z3 用于 MAX-SAT 的问题

Question

我对 MAX-SAT 很感兴趣，并希望 Z3 将其作为内置功能。有没有计划在不久的将来这样做？

在没有上述情况的情况下，我尝试从命令行使用示例 maxsat 应用程序。不幸的是，每当我执行 exec.sh“filename.z3”时，我总是得到以下响应:“正在检查硬约束是否可满足...结果:0”。我究竟做错了什么？我向您保证，此响应似乎完全独立于文件的实际内容。

最后，maxsat示例中的注释没有明确说明如何将约束标记为硬或软。硬约束应该是公式前面有 :formula，软约束应该是公式前面有 :assumption。那么，要将“(assert (> x 0))”标记为软的，我们究竟要把“:assumption”放在哪里呢？ (我已经阅读了关于硬约束和软约束的查询，但问题/响应似乎更多是在寻找不可满足的核心的背景下，而不是不可满足公式的“最大可满足核心”。)

Answer 1

Z3 发行版中的 MaxSAT 示例演示了如何使用 Z3 API 实现两种 MaxSAT 算法。该示例仍然使用旧的(已弃用的)API 来断言约束，但可以轻松修改它以使用新的求解器 API。示例应用程序读取 SMT 1.0 文件。但是，MaxSAT 函数可用于使用 C API 创建的公式。该脚本假定 :assumption字段是软约束并且:formula很难。这是一个小例子，其中 (> x 0) , (> y 0) , (< x y)和 (> x (- y 1))是软约束，(> (+ x y) 0)和 (< (- x y) 100)是很难的。示例应用程序返回 3 .也就是说，最多可以满足三个软约束。

(benchmark ex
  :extrafuns ((x Int))
  :extrafuns ((y Int))
  ;; Soft Constraints
  :assumption (> x 0)
  :assumption (> y 0)
  :assumption (< x y)
  :assumption (> x (- y 1))
  :formula 
  (and 
  ;; Hard Constraints
  (> (+ x y) 0)
  (< (- x y) 100)
))

也就是说，我们没有计划在 Z3 API 中直接支持 MaxSAT。在未来的版本中，我们可能会将 MaxSAT 示例移植到其他 API(.NET、Python 和 C++)。