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

[Leonardo de Moura]

Hi Vu,

No, Z3 is not a good option. The problem is too big.
BTW, converting the dimacs file into SMT-LIB formula will probably not help. The file will be much much bigger, and the memory consumption will increase.
Keep in mind that will have to create a "name" for each one of the 38 million variables. Just the symbol table for storing all these names will consume a lot of memory.
If you want to use SMT, one possibility is to encode the problem in another logic such as QF_BV (bit-vectors).
An encoding in QF_BV is usually much more compact, in particular, if you are encoding constraints such as a=b*c into CNF.

Cheers,
Leo

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of ThanhVu (Vu) Nguyen
Sent: Thursday, July 28, 2011 10:42 PM
To: SMT-LIB at cs.nyu.edu
Subject: Re: [SMT-LIB] fast SAT solver for very large instances

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,
>
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib