有人可以给我提供一些示例，这些示例可以使用SMT求解器（如microsoft z3）来解决，但不能由约束求解器（如gecode）来解决吗？约束求解器和SMT求解器之间的基本区别是什么？
约束求解器与SMT求解器
•
问答
iCMS 回答：约束求解器与SMT求解器
一般而言，SMT求解器可以处理许多有趣的理论：整数，实数，字符串，序列，集合，未解释的函数，数据类型，递归定义，线性和非线性算术...
您可以查看http://smtlib.cs.uiowa.edu/logics.shtml来了解受支持的常见逻辑。 SMT求解器的亮点在于如何在一个通用框架中自由混合和匹配来自这些域的约束。
我对Gecode并不十分熟悉，但我认为它更加专注，只关注一类约束。当然，这将使其对于预期的领域非常强大，但也意味着它们不具备SMT求解器提供的通用性。
如果您尝试“选择”一个，我建议根据具体情况决定：对于每个问题，您可能会发现获胜者可能是SMT解决方案或其他不基于SMT的约束解决方案-技术。我怀疑您是否可以“唯一”选择一个可能会遇到的问题。如果您发布感兴趣的特定问题，则可以获得更好的建议。