问题描述
有人可以给我一些可以使用 SMT 求解器(如 microsoft z3)求解但不能通过约束求解器(如 Gecode)求解的示例吗??约束求解器和 SMT 求解器之间的基本区别是什么?
can someone give me examples that can be solved using SMT solver ( like microsoft z3 ) but cant be solved by constraint solvers ( like Gecode ) ?? What is the basic difference between constraint solver and SMT solver?
推荐答案
总的来说，SMT 求解器可以处理许多感兴趣的理论:整数、实数、字符串、序列、集合、未解释函数、数据类型、递归定义、线性和非线性算术...
In general SMT solvers can handle many theories of interest: Integers, reals, strings, sequences, sets, uninterpreted functions, data-types, recursive definitions, linear and non-linear arithmetic...
你可以看看http://smtlib.cs.uiowa.edu/logics.shtml 查看支持的常用逻辑.SMT 求解器的亮点在于您可以如何在一个通用框架中自由混合和匹配来自这些域的约束.
You can take a look at http://smtlib.cs.uiowa.edu/logics.shtml to see the common logics that are supported. Where SMT solvers shine is how you can freely mix-and-match constraints from these domains in one common framework.
我对 Gecode 不是很熟悉，但我认为它更专注，只关注一类约束.当然，这将使它对于它所针对的领域非常强大，但也意味着它们没有 SMT 求解器提供的通用性.
I'm not terribly familiar with Gecode, but I presume it is much more focused, looking at only a class of constraints. This, of course, would make it very powerful for the domain it is intended for, but would also mean they don't have the generality offered by SMT solvers.
如果您想挑选"一个，我建议您逐案决定:对于每个问题，您可能会发现获胜者可能是 SMT 求解器或其他一些不基于 SMT 的约束求解器-技术.我怀疑您是否可以唯一地"为您可能遇到的任何问题选择一个.如果您发布您感兴趣的具体问题，您可以获得更好的建议.
If you are trying to "pick" one, I'd recommend deciding on a case-by-case: For each problem you might find the winner might be an SMT-solver or some other constraint solver that's not based on SMT-technology. I doubt you can "uniquely" pick one over the other for any problem you might have. If you post specific-questions you are interested in, you can get better suggestions.
这篇关于约束求解器与 SMT 求解器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！