TPPmark2014 http://imi.kyushu-u.ac.jp/lasm/tpp2014/tppmark2014-2.pdf の1問目、a^2 mod 3 ≠ 2 を証明するために a^2 - 3q = 2 の充足不能性(実行不能性)をソルバで示そうとしてみたが、Z3は「unknown」に、Gurobi 5.6.3 は「ERROR 10021: Quadratic equality constraints」に、SCIP-3.1.0は止まらなそうで、SCIP-2.1.1は巨大な値の誤った解を出力してしまった。 一般には決定不能である問題を解かせようとしているので、まあ仕方ない。
; TPPmark2014_1.smt2
(declare-fun a () Int)
(declare-fun q () Int)
(assert (>= a 0))
(assert (>= q 0))
(assert (= (+ (* a a) (* (- 3) q)) 2))
(check-sat)
\ TPPmark2014_1.lp
MINIMIZE
0 a
SUBJECT TO
- 3 q + [ a * a ] = 2
BOUNDS
a >= 0
q >= 0
GENERALS
a
q
END