将 Z3 用于 MAX-SAT 的问题 [英] Issues with utilizing Z3 for MAX-SAT
问题描述
我对 MAX-SAT 感兴趣，并希望 Z3 将其作为内置功能.在不久的将来有没有计划这样做?
I am interested in MAX-SAT and was hoping Z3 would have this as a built-in feature. Are there any plans to do this in the near future?
在没有上述情况的情况下，我尝试从命令行使用示例 maxsat 应用程序.不幸的是，每当我执行 exec.sh "filename.z3" 时，我总是得到以下响应:检查硬约束是否可满足...结果:0".我究竟做错了什么?我向您保证，此响应似乎与文件的实际内容完全无关.
In the absence of the above, I have tried using the example maxsat application from the command line. Unfortunately, whenever I do exec.sh "filename.z3", I always get the following response: "checking whether hard constraints are satisfiable...result: 0". What am I doing wrong? I assure you that this response appears to be quite independent of the actual contents of the file.
最后，maxsat 示例中的注释没有明确说明如何将约束标记为硬约束或软约束.硬约束应该是前面有 :formula 的公式，而软约束应该是前面有 :assumption 的公式.那么，要将(assert (> x 0))"标记为软，我们究竟把:assumption"放在哪里?(我已经阅读了关于硬约束和软约束的查询，但问题/响应似乎更多地是在寻找不可满足的核心的背景下，而不是不可满足公式的最大可满足核心".)
Finally, the comments in the maxsat example do not clearly specify how to mark constraints as hard or soft. A hard constraint is supposed to be a formula preceded by :formula, and a soft constraint a formula preceded by :assumption. So, to mark "(assert (> x 0))" as soft, where exactly do we put the ":assumption"? (I am have read the query about hard and soft constraints, but the question/response seemed to be more in the context of finding unsatisfiable cores, as opposed to "maximum satisfiable cores" of unsatisfiable formulas.)
推荐答案
Z3 发行版中的 MaxSAT 示例演示了如何使用 Z3 API 实现两个 MaxSAT 算法.该示例仍然使用旧的(不推荐使用的)API 来断言约束，但可以轻松修改它以使用新的求解器 API.示例应用程序读取 SMT 1.0 文件.但是，MaxSAT 函数可用于使用 C API 创建的公式.该脚本假定 :assumption 字段是软约束，而 :formula 是硬约束.这是一个小例子，其中 (> x 0)、(> y 0)、((> x (- y 1)) 是软约束，(> (+ xy) 0) 和 (<(- xy) 100) 是困难的.示例应用程序返回 3.也就是说，最多可以满足三个软约束.
The MaxSAT example in the Z3 distribution demonstrates how to implement two MaxSAT algorithms using the Z3 API. The example still uses the old (deprecated) API for asserting constraints, but it can be easily modified to use the new solver API. The example application reads a SMT 1.0 file. However, the MaxSAT functions can be used on formulas created using the C API. The script assumes that :assumption fields are soft constraints and :formula is a hard one. Here is a small example, where (> x 0), (> y 0), (< x y) and (> x (- y 1)) are soft constraints, and (> (+ x y) 0) and (< (- x y) 100) are hard ones. The example application returns 3. That is, at most three of the soft constraints can be satisfied.
(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++).
That being said, we do not have plans to support MaxSAT directly in the Z3 API. In future versions, we may port the MaxSAT example to other APIs (.NET, Python and C++).
这篇关于将 Z3 用于 MAX-SAT 的问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
