0

我正在使用 z3 (v4.3.1) 来解决包含未解释函数和量词的约束集。问题是z3的内存使用率很高。以下是我的约束：

(solver
(v0 0)
(forall ((i Int))
(let ((a!1 (=> (v0 i)
               (and (not (v1 i))
                    (not (v2 i))
                    (not (v3 i))
                    (not (v4 i))
                    (not (v5 i))))))
  (=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v0 i) (v1 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v1 i)
               (and (not (v0 i))
                    (not (v2 i))
                    (not (v3 i))
                    (not (v4 i))
                    (not (v5 i))))))
  (=> (>= i 0) a!1)))
forall ((i Int))
(let ((a!1 (=> (v1 i) (or (v2 (+ i 1)) (v5 (+ i 1))))))
  (=> (>= i 0) a!1)))
(forall ((i Int))
(let ((a!1 (=> (v2 i)
               (and (not (v0 i))
                    (not (v1 i))
                    (not (v3 i))
                    (not (v4 i))
                    (not (v5 i))))))
  (=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v2 i) (v3 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v3 i)
               (and (not (v0 i))
                    (not (v1 i))
                    (not (v2 i))
                    (not (v4 i))
                    (not (v5 i))))))
  (=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v3 i) (v4 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v4 i)
               (and (not (v0 i))
                    (not (v1 i))
                    (not (v2 i))
                    (not (v3 i))
                    (not (v5 i))))))
  (=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v4 i) (v1 (+ i 1)))))
(forall ((i Int))
(let ((a!1 (=> (v5 i)
               (and (not (v0 i))
                    (not (v1 i))
                    (not (v2 i))
                    (not (v3 i))
                    (not (v4 i))))))
  (=> (>= i 0) a!1)))
(forall ((i Int)) (=> (>= i 0) (=> (v5 i) (v5 (+ i 1)))))
(exists ((i Int)) (=> (>= i 0) (v5 i)))
(forall ((i Int))
(let ((a!1 (not (v5 (- (+ i 3) 1)))))
(let ((a!2 (=> (and (v0 i) (v1 (+ i 1))) a!1)))
  (=> (>= i 0) a!2))))
(forall ((i Int))
(let ((a!1 (not (v5 (- (+ i 4) 1)))))
(let ((a!2 (=> (and (v3 i) (v4 (+ i 1)) (v1 (+ i 2))) a!1)))

当我将约束集写入 smt2 文件并使用 z3 解决它时，我很快就得到了“未知”的结果。以下是 smt2 文件的内容

(declare-fun v0 (Int) Bool)
(declare-fun v1 (Int) Bool)
(declare-fun v2 (Int) Bool)
(declare-fun v3 (Int) Bool)
(declare-fun v4 (Int) Bool)
(declare-fun v5 (Int) Bool)
(assert (v0 0))
(assert  (forall ((i Int)) (=> (v0 i)     (and (not (v1 i)) (not (v2 i)) (not (v3 i))    (not (v4 i)) (not (v5 i))))))
(assert  (forall ((i Int)) (=> (v1 i)     (and (not (v0 i)) (not (v2 i)) (not (v3 i))   (not (v4 i)) (not (v5 i))))))
assert  (forall ((i Int)) (=> (v2 i)     (and (not (v1 i)) (not (v0 i)) (not (v3 i)) (not (v4 i)) (not (v5 i))))))
(assert  (forall ((i Int)) (=> (v3 i)     (and (not (v1 i)) (not (v2 i)) (not (v0 i)) (not (v4 i)) (not (v5 i))))))
(assert  (forall ((i Int)) (=> (v4 i)     (and (not (v1 i)) (not (v2 i)) (not (v3 i)) (not (v0 i)) (not (v5 i))))))
(assert  (forall ((i Int)) (=> (v5 i)     (and (not (v1 i)) (not (v2 i)) (not (v3 i)) (not (v4 i)) (not (v0 i))))))
(assert  (forall ((i Int)) (=> (>= i 0) (=> (v0 i) (v1 (+ i 1))))))
(assert  (forall ((i Int)) (=> (>= i 0) (=> (v1 i) (or (v2 (+ i 1)) (v5 (+ i 1)))))))
(assert  (forall ((i Int)) (=> (>= i 0) (=> (v2 i) (v3 (+ i 1))))))
(assert  (forall ((i Int)) (=> (>= i 0) (=> (v3 i) (v4 (+ i 1))))))
(assert  (forall ((i Int)) (=> (>= i 0) (=> (v4 i) (v1 (+ i 1))))))
(assert  (forall ((i Int)) (=> (>= i 0) (=> (v5 i) (v5 (+ i 1))))))
(assert  (exists ((i Int)) (=> (>= i 0) (v5 i))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (and (v0 i) (v1 (+ i 1))) (not (v5 (+ i 2)))))))
(assert (forall ((i Int)) (=> (>= i 0) (=> (and (v3 i) (v4 (+ i 1)) (v1 (+ i 2))) (not (v5 (+ i 3)))))))
(check-sat)

我只是想知道是我写错了还是z3很难解决这个问题。

4

1 回答 1

0

只有最后一个断言会导致问题，如果您将其从代码中删除，那么您将获得“sat”

于 2013-05-25T16:46:51.403 回答