SMT vs SAT

[Mark Engelberg]

I'm aware that SMT solvers can handle richer and more expressive formulations than SAT solvers. I understand SAT solvers but don't have experience with SMT solvers.

It looks to me at first glance that Picat expresses problems using the same constraint operators, regardless of the underlying solver. This leaves me wondering:

1) What sorts of Picat constraints are solved more efficiently by an SMT solver than an SAT solver?

2) Are there any SMT formulations that aren't expressible in Picat, but would be expressible if one were to directly use the underlying SMT solver without going through Picat, or is Picat's constraint system expressive enough to describe everything you can do with an SMT solver?

[Hakan Kjellerstrand]

1) I haven't tested all my constraint models with both SMT and SAT solvers, but in my experience there are not many problems that are generally faster with Picat's SMT module than Picat's SAT solver.  Sometimes SMT (especially the z3 solver) is faster for smaller instances but often SAT is then faster for larger problems.

 One example that I remember where SMT is faster than SAT (and CP) is Euler problem 345: http://hakank.org/picat/euler345.pi (see the timings in the model), though the MIP solver (CBC) is the fastest.

  It is quite nice that it's quite simple to test different solvers in Picat.

2) Note: Most of my knowledge of SMT is via Z3/Python and by converting my CP models to Z3, see http://www.hakank.org/z3/ (see comments below)

   SMT has some features that is not supported via Picat SMT module:

   * pop/push of the context of a model, e.g. incremental solving a model

   * soft constraints

   * arbitrary large integer/float types. For the SMT module, Picat supports only integers in the range -2**56..2**56.

  Note that Picat's SMT module does support SMT's logics, so one can play with this with the options of solve/2, e.g.

     solve($[z3,logic("QF_LIA"], Vars)

I should say that for my Z3/Python models, most of them are quite (often much) slower than my Picat models. In part this is because Z3 does not have support for certain global constraints such as cumulative, global cardinality, element etc so I had to implement them in Z3/Python. Though a different encoding might be faster.

--
You received this message because you are subscribed to the Google Groups "Picat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to picat-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/picat-lang/f34b1021-a281-437b-9591-1dda6b7ed114n%40googlegroups.com.

--

Hakan Kjellerstrand
http://www.hakank.org/
http://www.hakank.org/webblogg/
http://www.hakank.org/constraint_programming_blog/
http://twitter.com/hakankj
https://www.facebook.com/hakankj