利用Z3和SMT-LIB查找最高回文乘积

Question

在"Test-Only Development" with the Z3 Theorem Prover的基础上，我尝试在SMT-LIB中对Project Euler problem 4进行编码，并使用Z3解决它。

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

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

如何更改代码以找到906609的最大值？我尝试过使用(maximize (* p q))，但它报告了一个错误，显示为Objective function '(* p q)' is not supported。我可以调整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按原样运行会产生以下结果：

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

Answer 1

一种可能的解决方案是

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

Answer 2

其他可能的解决方案:我们搜索一个数字efggfe，它是数字9ab和9cd的乘积。使用代码

 (declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (= (* (+ 900 (* 10 a) b)  (+ 900 (* 10 c) d))      
           (+ (* 100000 e) (* 10000 f) (* 1000 g) (* 100 g) (* 10 f) e)))

(check-sat)
(get-model)

我们获得输出

sat 
(model 
(define-fun g () Int 6) 
(define-fun f () Int 0) 
(define-fun e () Int 9) 
(define-fun d () Int 3) 
(define-fun c () Int 1) 
(define-fun b () Int 3) 
(define-fun a () Int 9) )

其对应于数字906609。

请在线运行此代码here。

为了验证906609是否为最大值，我们运行以下代码

 (declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(assert (and (>= a 0) (<= a 9)))
(assert (and (>= b 0) (<= b 9)))
(assert (and (>= c 0) (<= c 9)))
(assert (and (>= d 0) (<= d 9)))
(assert (and (>= e 0) (<= e 9)))
(assert (and (>= f 0) (<= f 9)))
(assert (and (>= g 0) (<= g 9)))
(assert (= (* (+ 900 (* 10 a) b)  (+ 900 (* 10 c) d))      
           (+ (* 100000 e) (* 10000 f) (* 1000 g) (* 100 g) (* 10 f) e)    ) )
(assert (>  (+ (* 100000 e) (* 10000 f) (* 1000 g) (* 100 g) (* 10 f) e)        906609))           

(check-sat)

相应的输出是

unsat

请运行最后一段代码here