2017年6月8日木曜日

MSE2017 Testing

主催者が用意してくれたベンチマークがWeightedとUnweightedで各50個あり、SolverをUploadして、StarExeClusterにジョブを投げます。Permissionの問題がありましたが、主催者が対処してくれました。(ということは、他に未だ誰もテストしていない??? )

1)Archiveの仕方
まず躓いたのは、UploadでWrapperFolderを含めてはいけないことでした。普通にzipでやってしまうと含まれてしまうので、CurrentDirに入って、

tar cvf aaa.tar ./*

とやってtar FILEをつくり"upload solver"を実行します。

それから、TESTフォルダに入って"create_job"でソルバと動かしたいベンチマークのペアを指定します

2)staticに注意

基本的に実行ファイルは、-static でビルドされている必要があります。いきなり即終了したので変だなあと思ってログを見ると、*.soが見つからないというエラーで実行されていませんでした。StarExecは、古いLinuxらしいです。failureとして報告されないので、要注意です。ログは見るようにしましょう。

3)sigterm

InComplete部門は、SigTermが来たらSolutionをプリントすることになっていますが、どうも来ない疑いがあります。そこで、本来のTIMEOUT直前5秒前に発生させて実行しました。(90sec/300sec各トラック用にScriptを用意)

timout  85     ./EXE $1
timeout 295   ./EXE $1

これで一応いけることを確認しました。

その後、事務局より、現在、SIGTERMの後に数秒してSIGKILLするようにStarExecの管理者に依頼中とのことで、来週には改善されるだろうとのことです。

SIGTERMのDebug用として、runsolverを紹介されました。これ上で走らせれば、SIGTERMとSIGKILLを自由なタイミングで操作可能とのことでしたが、local machineで、fileに出力させながらやってみると、強制終了が、いくつかでていました。特にTIMEOUTのところで出ている訳ではないので不思議です。とりあえず、上記方策を、事務局に提案しておきました。

=>
その後、予想通り、SIGTERMとSIGKILLのDelayは、User責任になったようです。最終的には、以下のスクリプトで提出しました。displayの処理時間は、User責任なので、最後のflush(stdout)するのを忘れないようにしましょう。

#!/bin/sh
delay=5
wl=`expr $STAREXEC_WALLCLOCK_LIMIT - $delay`
#echo $STAREXEC_WALLCLOCK_LIMIT $wl
timeout $wl ./maxroster $1

最大インスタンス(d4.wcnfで、約1400万変数)でも殆ど時間がかかっていなかったので5秒も取る必要はなかったのかもしれません。

4)テストの確認
主催者が50インスタンスづつ用意してくれているので、それでcreate_jobで確認します。
なぜか、他の人のソルバーもテストすることも可能でした。

create_jobが終ると、job_informationで、CSVファイルをダウンロードします。
こんな感じです。
pair id benchmark benchmark id solver solver id configuration configuration id status cpu time wallclock time memory usage result optimum_solution hard_clauses optimum checker_solution checker given_solution
290700075 Weighted/1401.wcsp.dir.wcnf 4414170 maxroster 11897 default.sh 219868 complete 85 85.01 250044 -- 459106 satisfied FALSE 459111 ok 459111
290700076 Weighted/1401.wcsp.log.wcnf 4414171 maxroster 11897 default.sh 219868 complete 84.99 85.01 256424 -- -1 satisfied FALSE 467103 ok 467103
290700077 Weighted/1403.wcsp.dir.wcnf 4414172 maxroster 11897 default.sh 219868 complete 85.01 85.01 248172 -- 459246 satisfied FALSE 459274 ok 459274

chekerの計算した値<=自分のソルバーが計算した値になっていることを確認します。

5)所感
締め切りの2日前になってもカテゴリーやらスクリプトが変わりました。オーガナイザが変わったので致し方ない面があるかと思います。来年からは、今年の経験を元に改善されることでしょう。

=>
締め切り日が変更され2週間遅れます。

結果は、SAT2017で発表されるそうです。










2017年6月1日木曜日

MaxSAT Competition 2017 のIncompleteのルール

事務局に問い合わせたので、メモしておきます。

60秒と300秒は、別なトラックになります。各々Unweight/Weightのカテゴリーがあるので,好きな方(もしくは両方)に参加してもよい。

Webには、

 Incomplete score:
    ∑i ∈ instances (cost of solution for i found by solver)
                      / (cost of best solution for i found by any solver)

現実には、こういうことらしい。

Σ i ∈ instances A Score

A Scoreは、best_solutionのとき1、それ以外は0、従い、virtual best solverのスコアは、インスタンス数になる。(スコアが高いほど1位を取ったインスタンス数が多い)