constraint-programming - SMT-solver 在约束求解方面比 CSP-solver 有什么优势？

Question

SMT-Solver 可用于约束求解。众所周知，CSP 求解器多年来也用于约束求解。那么 SMT 求解器相对于 CSP 求解器的优势是什么？

Answer 1

这完全取决于你想做什么。您可以将两者转换为 SAT 并将约束问题作为 SAT 问题来解决。在建模问题时，约束求解器通常提供最高级别的抽象。SAT 求解器非常快，但根据您的问题，SMT 或约束求解器可能更快。

您的问题没有一般性的答案。这取决于您的特定用例。