Are there any guidelines for how to recognize, for a given problem, which approach is more likely to yield good results? SAT solver or SMT solver? Is there any guidance anyone can offer about which sorts of problems can be handled better by SAT solvers than by SMT solvers, or vice versa?

  • $\begingroup$ There are a variety of solvers. But no one knows which will give better result. No one even knows why oftenly SAT is solved fast (except cases when you pick first two literals in each clause and solve given 2-SAT and it's satisfiable). $\endgroup$ – rus9384 Sep 10 '17 at 16:30
  • $\begingroup$ What does this question mean? Eager SMT vs lazy? Or literally SAT vs SMT (in which case how does it make sense? they solve different problems) $\endgroup$ – harold Sep 10 '17 at 17:28
  • $\begingroup$ See cs.stackexchange.com/q/12325/755 and cs.stackexchange.com/q/12087/755 for some related discussion. $\endgroup$ – D.W. Sep 11 '17 at 5:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.