使用 Z3 和 SMT-LIB 查找最高回文积答案

【问题标题】：Using Z3 and SMT-LIB to find highest palindromic product使用 Z3 和 SMT-LIB 查找最高回文积
【发布时间】：2015-03-28 07:17:14
【问题描述】：

基于"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)
)

【问题讨论】：

使用maximize需要构建Z3的优化分支。寻找最大值的另一种可能的解决方案是断言没有更小的解决方案。我从来没有为 Euler 4 工作过（请参阅我博客上的 cmets），但我对 this somewhat simpler problem 使用了类似的解决方案。
是的，我设法找到了 opt 分支，而且我对理论 CS 知之甚少，无法知道为什么最大化不起作用（似乎抱怨不支持乘法；我想这必须与我们在复杂性树中处于高位这一事实有关）。

标签： math z3 smt

【解决方案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。

【讨论】：

虽然这行得通，但它不是我想要的。我可以调整任何变量（p、q、pq、a 等）以获得我知道的答案。我正在寻找的是一种编码约束的方法，即在给定其他约束的情况下，produkt pq 应该是尽可能高的。想象一下，我事先不知道答案，并希望自动找到答案。

【解决方案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

【讨论】：

你不是隐藏了一个要求，即数字应该由两个因素组成，每个因素都大于 900？ (* (+ 900 (* 10 a) b) (+ 900 (* 10 c) d)) ?是的，这行得通，但我们仍然在给 Z3 强烈的暗示，我们只能在事后才知道。我希望我们可以让 Z3 说“这是最大的”，而不必重新运行。难道不能使用push 和pop 来做类似的事情吗？非常感谢你的好答案，但这并不是我想要的。