[SMT-LIB] fast SAT solver for very large instances

[ThanhVu (Vu) Nguyen]

Hi all, I am asking for someone about an efficient SAT solver for very
large instances -- his query is listed below.  Would Z3 be a good
candidate ?   Thanks,



------


I have been using minisat, a sequential solver, for most of my
instances, and it worked quite well until the problems got too
big. The instance I'd like to solve has 38 million variables and 180
million clauses.

We have a 24-core machine with 32GB, and I did try lingeling, which is
a parallelized solver, but I hit the memory limit even sooner trying
to use multiple solver threads.


Vu,