[SMT-COMP] dual-core for SMT-COMP 2010?

[Johannes Waldmann]

Aaron Stump wrote:

> I'm writing to ask your opinion about whether or not we should enable the
> dual-core feature of our cluster (www.smtexec.org) for SMT-COMP 2010.

Just a data point: since 2008,
the Termination Competition runs on a 16 core machine.
(termination provers are run one after another,
and each can use all cores.)

http://termination-portal.org/wiki/Termination_Competition

I think most termination provers do really use several cores,
but my impression is that they just run several instances
of some SMT (well, mostly SAT) solver (for different problems),
each of them running on a single core.

I would hope that calling one instance of a multi-core SMT solver
for the disjunction of the problems should be more efficient.

So, I'm looking forward to multi-core SMT solvers.

Best regards, Johannes Waldmann.



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
Url : /pipermail/smt-comp/attachments/20091231/ca904964/signature.bin