1

我正在尝试在线使用 Z3 SMT-LIB 解决一些最大/最小问题。

一个例子是：

找到两个和为 9 的非负数，使得一个数与另一个数的平方的乘积最大。

经过多次尝试，构建了以下代码

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

在此处在线运行此示例

如果您对此问题有更有效的代码，请告诉我。非常感谢。

4

0 回答 0