Max-SAT evaluation 2015 へ投稿した自分のソルバ、テスト環境では動作したけれど、クラスタのノードでは動作していないとか。 何が原因なんやろ……
以下、主催者からのメールから抜粋。
-----------
We have a problem with your solvers toysat and toysat_ls. The solvers run fine in several machines (e.g., in the cluster front end), giving the right solution for the tested instances. But not in the cluster nodes, where the evaluation is run. The solvers start taking memory without any output in the shell, until reach the maximum memory permitted, 3.5 GB.
The nodes CPUs are:
Intel(R) Xeon(R) CPU E5-2620 0 @ 2.00GHz
The nodes are Linux CentOS release 6.5.
If I was correct, the problem was conversion failure between external encoding and Unicode.
When toysat processes command line arguments, it tries to convert them from external encoding into Unicode. If the conversion failed, it tries to print the error to stderr and quit, but printing the error itself involves converting Unicode error message into external encoding. It causes the same error again and loops infinitely.
Locale encoding is used as the default external encoding, and if the encoding is not built-in supported encodings (i.e. utf-8, utf-16, utf-32, iso-8859-1), iconv() is used for conversion. And iconv() loads shared object usually from /usr/lib/x86_64-linux-gnu/gconv directory using dlopen(). I guess that the loading was failed, because the file is missing or due to glibc compatibility problem (i.e. using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking).
Last year's version of toysat explicitly specified iso-8859-1 as the external encoding to avoid potential such problems and to speed up I/O. But I forgot to enable the code this year...