Z3 中的软/硬约束 [英] Soft/Hard constraints in Z3

问题描述

如何在 Z3 中表达软约束和硬约束?我从 API 知道可以有假设(软约束)，但是在使用命令行工具时我无法表达这一点.我使用 z3/smt2/si

How do I express soft and hard constraints in Z3? I know from the API that it is possible to have assumptions (soft constraints), but I can't express this when using the command line tool. I am calling it using z3 /smt2 /si

推荐答案

假设在 SMT 2.0 前端可用.它们用于提取不可满足的核心.它们还可用于撤回"假设.请注意，假设并不是真正的软约束"，但它们可以用来实现它们.请参阅 Z3 发行版中的 maxsat 示例 (subdir maxsat).话虽如此，下面是一个关于如何在 Z3 SMT 2.0 前端使用假设的示例.

Assumptions are available in the SMT 2.0 frontend. They are used to extract unsatisfiable cores. They may be also used to "retract" assumptions. Note that, assumptions are not really "soft constraints", but they can be used to implement them. See the maxsat example (subdir maxsat) in the Z3 distribution. That being said, here is an example on how to use assumptions in the Z3 SMT 2.0 frontend.

;; Must enable unsat core generation
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
;; Declare three Boolean constants to "assumptions"
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
;; We assert (=> p C) to track C using p
(declare-const x Int)
(declare-const y Int)
(assert (=> p1 (> x 10)))
;; An Boolean constant may track more than one formula
(assert (=> p1 (> y x)))

(assert (=> p2 (< y 5)))
(assert (=> p3 (> y 0)))

(check-sat p1 p2 p3)
(get-unsat-core) ;; produce core (p1 p2)

(check-sat p1 p3) ;; "retrack" p2
(get-model)

这篇关于Z3 中的软/硬约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！