title: Using Z3 and SMT-LIB to find highest palindromic product
body: <p>Based on <a href="http://blogs.teamb.com/craigstuntz/2014/07/07/38818/" rel="nofollow">"Test-Only Development" with the Z3 Theorem Prover</a>, I'm trying to encode <a href="https://projecteuler.net/problem=4" rel="nofollow">Project Euler problem 4</a> in SMT-LIB and solve it using Z3.</p>
  
  <p>The problem is to find the largest palindromic integer product of two three-digit numbers. The solution is <code>993 * 913 = 906609</code>.</p>
  
  <p>In the code below, I've only been able to encode that two three-digit numbers should be palindromic. This produces the correct, but not maximal, value of <code>604406</code>.</p>
  
  <p>How can I change my code so that the maximal value of <code>906609</code> is found?
  I've tried using <code>(maximize (* p q))</code>, but that reports an error, saying <code>Objective function '(* p q)' is not supported</code>.  I can tweak the range of <code>a</code>, but I'm looking for a way to have Z3 do that for me.</p>
  
  <p>What I have so far is:</p>
  
  <pre><code>(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
    (&lt;= 1 a 9)
    (&lt;= 0 b 9)
    (&lt;= 0 c 9)
  
    (&lt;= 100 p 999)
    (&lt;= 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)
  </code></pre>
  
  <p>Running this with <code>z3 -smt2 e4.smt2</code> as-is produces:</p>
  
  <pre><code>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)
  )
  </code></pre>