【发布时间】：2012-05-22 00:50:57
【问题描述】：
SMT-Solver 可用于约束求解。众所周知，CSP 求解器多年来也用于约束求解。那么 SMT 求解器相对于 CSP 求解器的优势是什么？
【问题讨论】：
标签： constraint-programming satisfiability
【发布时间】：2012-05-22 00:50:57
【问题描述】：
这完全取决于你想做什么。您可以将两者转换为 SAT 并将约束问题作为 SAT 问题来解决。在对问题进行建模时，约束求解器通常提供最高级别的抽象。 SAT 求解器非常快，但根据您的问题，SMT 或约束求解器可能更快。
您的问题没有通用答案。这取决于您的特定用例。
【讨论】：
-
是的，你是对的，谢谢你~我想知道什么时候 SMT 求解器比 CSP 求解器运行得更快？或者什么样的问题更适合 SMT 求解器，反之亦然？ SMT求解器是否可以处理CSP求解器可以很好处理的优化问题？
-
约束和 SMT 都可以处理优化问题，尽管我相信实际求解器中对此的支持在约束中更为常见。当 SMT/约束/SAT 更好/更快/时，没有固定的规则。这确实取决于您要解决的实际问题。
-
与约束求解器相比，SMT 求解器更通用，因此覆盖范围更大。