z3 - Z3 中的软/硬约束

Question

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

Answer 1

SMT 2.0 前端提供了假设。它们用于提取无法满足的核心。它们也可用于“撤回”假设。请注意，假设并不是真正的“软约束”，但它们可以用来实现它们。请参阅 Z3 发行版中的 maxsat 示例（subdir maxsat）。话虽如此，这里有一个关于如何在 Z3 SMT 2.0 前端使用假设的示例。

;; 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)