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)