3

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

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

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

4

1 回答 1

2

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++）。

于 2012-05-22T01:07:09.163 回答