z3 - 约束求解器与 SMT 求解器

Question

有人可以给我一些可以使用 SMT 求解器（如 microsoft z3）解决但不能由约束求解器（如 Gecode）解决的示例吗？约束求解器和 SMT 求解器的基本区别是什么？

Answer 1

一般来说，SMT 求解器可以处理许多感兴趣的理论：整数、实数、字符串、序列、集合、未解释函数、数据类型、递归定义、线性和非线性算术......

您可以查看http://smtlib.cs.uiowa.edu/logics.shtml以查看支持的常见逻辑。SMT 求解器的亮点在于您如何在一个通用框架中自由混合和匹配来自这些域的约束。

我对 Gecode 不是很熟悉，但我认为它更加专注，只关注一类约束。当然，这将使它在它所针对的领域非常强大，但也意味着它们不具备 SMT 求解器提供的通用性。

如果您要“选择”一个，我建议您逐案决定：对于每个问题，您可能会发现获胜者可能是 SMT 求解器或其他不基于 SMT 技术的约束求解器。我怀疑您是否可以“独特地”选择一个来解决您可能遇到的任何问题。如果您发布您感兴趣的特定问题，您可以获得更好的建议。