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

[Michael Tautschnig]

[...]
> 
> Right,  if one of them is false then the entire formula is false  --
> but the reverse is not true .    So the technique is also useful when
> most of the time the formula is unsat.
> 

That seems to be a somewhat naive claim: this will only work if the
unsatisfiable core of your formula is a subset of one of the parts that you
split the formula into. In general, this cannot be the case.

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/71554a0d/attachment-0001.asc>