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

【问题标题】：Which is better practice in SMT: to add multiple assertions or single and?SMT 中哪个是更好的做法：添加多个断言还是单个 and？
【发布时间】：2014-07-12 08:57:17
【问题描述】：

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

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

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

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

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

【问题讨论】：

标签： smtp z3 smtplib smt sat-solvers

【解决方案1】：

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

【讨论】：