There is an update on the HW:
We plan to run the competition on a cluster at Aalto University. We will have exclusive access to 32 nodes of 2x Six-Core AMD Opteron 2435 2.6GHz with at least 16 GB of RAM. This would mean 12 cores for each solver per benchmark, memory limit around 15 GB and time limit of 900 seconds. As fall back we have the cluster at JKU with the same characteristics as in the last years.
Beside the requirement to produces witnesses, rules, input and output format did not change. Please consult the pages of HWMCC'12 for more details. There is one exception though. We want to reuse the new Oski benchmarks submitted and used in 2013. But those have uninitialized latches. Thus you should assume pre AIGER 1.9 format but should be able to handle latches. If you are not able to support this feature let us know. There is also a new version of the AIGSIM tool available in the new release aiger-1.9.9.tar.gz which works more smoothly in this context, particularly when using bad state constraints as outputs.
This previous paragraph is an excerpt of the competition home page. So please be prepared to see uninitialized latches in the single and deep bound track. If you can not support this feature let us know as soon as possible. Note, that already for those discussed benchmarks we replaced 1 initialized by 0 initialized latches. Thus even though it is not a big deal to implement 1 initialized latches (if you have already 0 initialized and non-initialized), we will not use 1 initialized latches in the single and deep bound track.
Finally the 'aigreset' tool can be used to change or check initialization (the latter with the '-c' option), e.g.
$ aigreset -c oski1rub04.aig
*** [aigreset] latch 51 literal 22994 uninitialized