SAT解决方案是否有一个名称，其中部分公式是静态的（形成命题“理论”）并用作测试相对较小句子的可满足性的静态上下文。
许多这样的测试需要用不同的句子执行，因此每次重新评估每个小公式与静态部分的连接是次优的。
与增量 SAT 相比，可满足的句子不会附加到理论中，而是在测试后丢弃。
有没有适合这种情况的工具？
问问题
28 次
1 回答
0
不确定这是否有正式名称，但在 SMTLib 用语中，它被称为check-sat-assuming. 请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf的第 4.2.5 节（第 64 页）
于 2018-05-18T15:55:36.543 回答