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

[Tinelli, Cesare]

Vu,

On 29 Jul 2011, at 18:31, Leonardo de Moura 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.

A way to avoid the symbol table could be to use an SMT-LIB logic with integers and declare a function symbol from Int to Bool, to represent atoms, e.g.,

(declare-fun a (Int) Bool)

and then use the DIMACS atoms (which are numbers) as indices. For example, the DIMACS clause 

1 -3 7 0

would become

(or (a 1) (not (a 3)) (a 7))

In any case, the resulting formula is going to be bigger byte-wise than the DIMACS one. Also, there is not much use in running an SMT solver on a purely Boolean problem. I doubt there is any SMT solver that is more performant than a state-of-the-art SAT solver on SAT problems.

> 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.
> 
Leonardo is right of course. To harness the power of SMT solvers you want to use an encoding of your original problems in a more expressive logic than propositional logic.

Cheers,


Cesare



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