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

[Michael Tautschnig]

Hi Vu,

> 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.
> 

You might want to tell us a bit more about what these instances actually
describe to provide you with helpful feedback. And, given that you suggested
splitting, you might also want to say what you want to learn from the result.

Obviously splitting will only yield a conclusive answer if your 10 subproblems
are expressed over disjoint sets of variables. Otherwise, yes, if one of them
returns false the entire formula is false, but the converse clearly isn't valid.

Best,
Michael


-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 833 bytes
Desc: not available
URL: </pipermail/smt-lib/attachments/20110729/5581fb7a/attachment.asc>