Z3中关于增量SAT的一些问题：它可以被停用吗？里面使用了哪些技术？

Question

我还在学习Z3的胆量（Python）。

我注意到 Z3 默认执行增量 SAT 求解（参见）：具体来说，每次使用 s.add命令（其中 s 是一个求解器），这意味着它将那个子句添加到 s，但它不会忘记你之前学到的一切。

第一个问题：Z3可以做非增量SAT求解吗？也就是说，不知何故 'deactivate' 增量求解。这意味着什么？我们正在为每个放大的公式创建一个新的求解器？

例如，这种方法是 Z3-default-incremental:

...
  phi = a_formula
  s = Solver()
  s.add(phi)
  while  s.check() == sat: 
    s.check()
    m = s.model()
    phi = add_modelNegation(m)
    s.add(phi) #in order not to explore the same model again
  ...

也就是说，一旦我们得到一个模型，我们就将否定的模型附加到相同的求解器。

虽然这个 'forcing' Z3 是非增量的：

...
  phi_st = a_formula
  s = Solver()
  s.add(phi_st)
  negatedModelsStack = []
  while  s.check() == sat:
    m = s.model()
    phi_n = add_modelNegation(m)
    negatedModelsStack.append(phi_n)
    original_plus_negated = And(phi_st, And(negatedModelsStack))
    s = Solver()
    s.add(original_plus_negated) #in order not to explore the same model again
  ...

也就是说，一旦我们得到一个模型，我们就将获得的模型附加到一个新的求解器。

我说得对吗？

另一方面，在附件link中，声明如下：

将其与 CVC4 等进行比较；默认情况下不是增量的。如果你想在增量模式下使用 CVC4，你必须传递一个特定的命令行参数

这是否意味着在 CVC4 中您每次都必须创建一个新的求解器？就像在第二个代码中一样？

第二个问题：我如何才能确切知道我在 Z3 中使用什么技术进行增量求解？我一直在阅读增量 SAT 理论，我看到其中一种技术是 'CDCL'（http://www.cril.univ-artois.fr/~audemard/slidesMontpellier2014.pdf），这是否用于 Z3 的增量搜索？

参考文献： 为了不让 Stack 被类似的问题淹没，您一般推荐哪些阅读增量 SAT，特别是 Z3 的增量 SAT？另外，Z3 的增量 SAT 是否与其他求解器（如 MiniSAT 或 PySAT）相似？

Answer 1

我不确定您为什么要让 z3 以非增量方式运行。但是，如果那是您的目标，请不要多次调用 check：这等同于非增量。（将增量视为“附加功能”。您不必使用它。z3 和 cvc4 之间的唯一区别是后者需要您提前告诉它您打算以增量方式使用它，而前者默认情况下是增量的。）作为最终用户，您真的不需要知道或关心差异。

旁注如果你启动 cvc4 时没有告诉它是增量的并调用 check 两次，它会抱怨。 z3不会。但除此之外，体验应该是一样的。

从编程的角度来看，我不认为了解求解器如何逐步实施真的很有帮助。（如果您正在实施自己的 SMT 求解器，这当然是最重要的。）网上有许多关于 SMT 的许多方面的论文，但如果您想从头开始研究该主题，我推荐 Daniel 和 Ofer 的关于决策程序的书：http://www.decision-procedures.org

Z3中关于增量SAT的一些问题：它可以被停用吗？里面使用了哪些技术？

Some questions about incremental SAT in Z3: can it be deactivated? Which techniques are used inside?

z3

z3py

theorem-proving

sat

satisfiability