首页 文章

在z3 smt2中使用整数除法时未知

提问于
浏览 次
1

我试图找到函数penta（n）=（n *（3n -1））/ 2的解，并且其中penta（z）= penta（a）penta（b）表示所有数量的正数 . 这可以工作，直到整数除法（div）是定义的一部分，但当它在定义中添加时，我得到了超时或未知 . 我希望能得到8,7,4 . 我对错误的做法有什么看法？

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

(define-fun penta ((n Int)) Int (div (* (- (* 3 n ) 1) n) 2) )  

(assert (= (penta z) (+ (penta a) (penta b))  ))
(assert (> a 1))
(assert (> b 1))
(assert (> z 1))

(check-sat)
(get-model)

我使用http://rise4fun.com/Z3网站上的版本和版本4.1（x64） .

z3

1 回答

  • 2

    主要问题是该问题使用两个非数字参数之间的整数乘法 . 一般的丢番图问题没有决策程序，所以Z3尽力而为，这不利于模型枚举 .

    当你不使用整数除法时，Z3会尝试基于将问题转换为有限域位向量来寻找模型的部分启发式算法 . 它通过对公式执行语法检查来调用此启发式方法 . 使用运算符时，语法检查失败（div ... 2） . 您可以编码（div x 2），以便启发式通过引入新变量并对其进行限制来解决问题：

    (declare-const penta_z Int)
(declare-const penta_a Int)
(declare-const penta_b Int)
(assert (or (= (* 2 penta_z) (penta z)) (= (+ 1 (* 2 penta_z)) (penta z))))
(assert (or (= (* 2 penta_a) (penta a)) (= (+ 1 (* 2 penta_a)) (penta a))))
(assert (or (= (* 2 penta_b) (penta b)) (= (+ 1 (* 2 penta_b)) (penta b))))
(assert (= penta_z (+ penta_a penta_b)  ))
(assert (> a 1))
(assert (> b 1))
(assert (> z 1))
(assert (>= penta_z 0))
(assert (<= penta_z 100))

    你也可以使用位向量直接编码你的问题，虽然这开始容易出错，因为你必须处理如何处理溢出 .

    回复于

相关问题