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

[ThanhVu (Vu) Nguyen]

thanks Leonardo ,  the reason I want to convert to smt-lib because I
want to try it on solvers such as cvc or z3.

do you have suggestions on how to deal with such large instances ?   I
was thinking about splitting it into say 10 parts and run them one by
one,  any of them returns false means the entire formula is false.



Vu,



On Fri, Jul 29, 2011 at 10:31 AM, Leonardo de Moura
<leonardo at microsoft.com> wrote:
> 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
>