约束求解器与SMT求解器

Question

有人能给我举一些例子，这些例子可以用SMT求解器(比如microsoft z3 )来解决，但是不能通过约束求解器(比如Gecode )来解决吗？约束求解器和SMT求解器的基本区别是什么？

Answer 1

通常，SMT求解器可以处理许多感兴趣的理论:整数、reals、字符串、序列、集合、未解释函数、数据类型、递归定义、线性和非线性算法.

您可以查看http://smtlib.cs.uiowa.edu/logics.shtml以查看所支持的公共逻辑。SMT解决方案的亮点在于如何在一个公共框架中自由地混合和匹配来自这些域的约束。

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

如果你试图“挑选”一个，我建议逐案决定:对于每一个问题，你可能会发现胜利者可能是一个SMT解决者或其他不基于SMT技术的约束解决器。我怀疑你是否能够“独一无二”地为你可能遇到的任何问题选择一个而另一个。如果你贴出你感兴趣的具体问题，你可以得到更好的建议。