SMT求解器优于CSP求解器在约束求解中的优势是什么？

Question

SMT-Solver可用于约束求解.众所周知,CSP求解器也用于求解约束多年.那么SMT求解器优于CSP求解器的优势是什么？

Answer 1

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

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