smtp - SMT 中哪个是更好的做法：添加多个断言还是单个 and？

Question

假设我有两个要在 SMT 中建模的子句，最好将它们添加为单独的断言，例如

(assert (> x y))
(assert (< y 2))

或者像这样使用 and 运算符添加一个断言

(assert (and 
(> x y)
(< y 2)
))

这对于 SMT 求解器性能方面的大规模问题是否重要。我正在使用 Z3。

Answer 1

连词被分成多个断言，所以它并不重要。如果您引入一个大合取，Z3 的解析器将创建一个包含所有合取的术语，但这只是维护合取之上的恒定开销。