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

[ThanhVu (Vu) Nguyen]

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

I'll try to ask my friend who is the one doing this for a more precise
description of what he's doing.

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

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.



> Best,
> Michael
>
>
>