数学 – 使用Z3和SMT-LIB找到最高的回文产品

2019年8月5日 273次阅读

基于
“Test-Only Development” with the Z3 Theorem Prover,我试图在SMT-LIB中编码
Project Euler problem 4并使用Z3解决它.

问题是找到两个三位数字的最大回文整数乘积.解决方案是993 * 913 = 906609.

在下面的代码中,我只能编码两个三位数字应该是回文.这会产生正确但不是最大值604406.

如何更改代码以便找到最大值906609？
我尝试过使用(最大化(* p q)),但报告错误,说不支持目标函数'(* p q)’.我可以调整a的范围,但我正在寻找让Z3为我做这件事的方法.

到目前为止我所拥有的是：

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(declare-const p Int)
(declare-const q Int)

(declare-const pq Int)

(define-fun satisfy ((pq Int)) Bool
 (and
  (<= 1 a 9)
  (<= 0 b 9)
  (<= 0 c 9)

  (<= 100 p 999)
  (<= p q 999)

  (= pq
     (* p q)
     (+ (* 100001 a)
        (*  10010 b)
        (*   1100 c)))))

(assert (satisfy pq))

; Does not work:
;(maximize (* p q))

(check-sat)
(get-model)

使用z3 -smt2 e4.smt2 as-is运行它会产生：

sat
(model
  (define-fun q () Int
    913)
  (define-fun p () Int
    662)
  (define-fun c () Int
    4)
  (define-fun b () Int
    0)
  (define-fun a () Int
    6)
  (define-fun pq () Int
    604406)
)

最佳答案 一种可能的解决方案是

    (declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(declare-const p Int)
(declare-const q Int)

(declare-const pq Int)

(define-fun satisfy ((pq Int)) Bool
 (and
  (<= 1 a 9)
  (<= 0 b 9)
  (<= 0 c 9)

  (<= 100 p 999)
  (<= p q 999)

  (= pq
     (* p q)
     (+ (* 100001 a)
        (*  10010 b)
        (*   1100 c)))))

(assert (satisfy pq))
(assert (> pq 888888))


(check-sat)
(get-model)

并且相应的输出是

sat
(model 
(define-fun pq () Int 906609) 
(define-fun q () Int 993) 
(define-fun p () Int 913) 
(define-fun c () Int 6) 
(define-fun b () Int 0) 
(define-fun a () Int 9) )

请在线运行此代码here.

点赞