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

[ThanhVu (Vu) Nguyen]

also is there an efficient tool to convert CNF Dimacs format to smtlib
format ?   thankx

Vu,



On Thu, Jul 28, 2011 at 8:43 PM, ThanhVu (Vu) Nguyen <tnguyen at cs.unm.edu> wrote:
> 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,
>