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

[Leonardo de Moura]

Hi Vu,

Just converting a dimacs file into a SMT-LIB file will not help. The generated SMT-LIB file will be just a CNF formula encoded in a different format.
CVC and Z3 are based on SAT technology, and they will also fail like minisat and lingling.
To effectively use SMT, you need to encode your problem in one of the logics available in SMT.
SMT-LIB format is much richer than the dimacs format.
If you try a higher level encoding, it will probably be more compact.
For example, you may try to use bit-vectors instead of Boolean variables.
Another possibility is to use quantifiers. 
One of the advantages of SMT is that you can create more compact encodings.  
What kind of problem are you trying to solve?

Cheers,
Leo

-----Original Message-----
From: nguyenthanhvuh at gmail.com [mailto:nguyenthanhvuh at gmail.com] On Behalf Of ThanhVu (Vu) Nguyen
Sent: Friday, July 29, 2011 9:58 AM
To: Leonardo de Moura
Cc: SMT-LIB at cs.nyu.edu
Subject: Re: [SMT-LIB] fast SAT solver for very large instances

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
>