search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
179 stars 44 forks source link

Pure Java solving suggestion #204

Closed uncttao closed 4 years ago

uncttao commented 4 years ago

Hi Devs, I have been using this awesome library for a while now. However, my experience so far indicates Z3 as the only respectable option in terms of performance in my settings. Yet trying to put Z3 up in my production environment is a real pain. I have tried pure JVM solvers such as Princess and SMTInterpol, but they are just way too slow. Could you please give me some suggestions on how to possibly squeeze every last drop of performance out of Princess or SMTInterpol? I only do pure boolean SAT solving, so maybe passing some configuration parameters helps? What options should I pass then in that case? Thanks a lot!

kfriedberger commented 4 years ago

Hi Tao, it is always nice to get feedback from users. Most questions and their solution are beneficial for all users.

We know that Princess is not the fastest SMT solver. It is also not used that often in our production environment. SMTInterpol is reasonably fast, but misses some options and feature to fine-tune it. SMTInterpol is mostly optimized for integer-based logics like LIA. To our knowledge, SMTInterpol does not support special features for boolean satisfiability such as internal formulae rewriting or AIG conversion.

The fastest SMT solvers (of course that depends on the query) are MathSAT5 and Z3. CVC4 and Boolector are also quite fast for boolean formulae. All of them are native libraries written in C/C++, mature and more otimized than the others mentioned.

For MathSAT5 and Z3, we are currently working on Windows support in a branch. What kind of problems did you experience when installing Z3? Software/hardware problems, installation problems or licensing issues? Are you using a build system like Maven or Ant?

Best, Karlheinz

uncttao commented 4 years ago

Thanks for the reply! The reason I couldn't deploy Z3 was a purely bureaucratic one; my enterprise cloud environment can only host pure JVM processes with no native application support. To have Z3 running would mean to break away from my enterprise CICD routine and set up my own ad-hoc cloud infrastructure, which is very inelegant and painful. Not to mention this is a part of a microservice so it complicates the issue even more.

uncttao commented 4 years ago

I am closing this issue because I ended up resolving the bureaucracy through a higher-level communication channel. I was almost thinking about porting some core Z3 into Java as the last resort. Thank you for the comment nevertheless!