Z3 SMT-LIB オンラインを使用して、いくつかの最大/最小の問題を解決しようとしています。
一例は次のとおりです。
合計が 9 で、一方の数値と他方の数値の 2 乗の積が最大になる 2 つの非負の数値を見つけます。
多くの試みの後、次のコードが構築されました
(define-fun f ((x Real) (y Real)) Real
(if (not (= y 0.0))
(* y (^ x (- y 1)))
0.0))
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(declare-const v Real)
(simplify (* x (^ (- 9 x) 2)) :som true)
(assert (= y (* 81.0 (f x 1))))
(assert (= z (* 18.0 (f x 2))))
(assert (= v (f x 3)))
(assert (= z (+ y v )))
(assert (not (= x 0)))
(assert (not (= x 9)))
(set-option :pp-decimal true)
(apply (then simplify solve-eqs))
(check-sat)
(get-model)
出力は次のとおりです。
(+ (* 81.0 x) (* (- 18.0) x x) (* x x x))
(goals
(goal (= (* 36.0 x) (+ (* 81.0 (^ x 0.0)) (* 3.0 (^ x 2.0))))
(not (= x 0.0))
(not (= x 9.0))
:precision precise :depth 2) )
sat
(model
(define-fun x () Real 3.0)
(define-fun v () Real 27.0)
(define-fun z () Real 108.0)
(define-fun y () Real 81.0) )
ここでこの例をオンラインで実行します
この問題に対するより効率的なコードがあれば教えてください。どうもありがとう。