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"でソルバと動かしたいベンチマークのペアを指定します

２）staticに注意

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

３）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秒も取る必要はなかったのかもしれません。

４）テストの確認
主催者が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の計算した値<=自分のソルバーが計算した値になっていることを確認します。

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

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

結果は、SAT２０１７で発表されるそうです。

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のとき１、それ以外は０、従い、virtual best solverのスコアは、インスタンス数になる。（スコアが高いほど1位を取ったインスタンス数が多い）　

ベンチマークテスト更新

池上先生が公開されているベンチマークをプロジェクト変換して、アップしていたのですが、
池上先生から、KnownBestValueと違うよ、と指摘されました。見直した結果、変換に酷いバグがあることが判明したので、バグ修正しました。最新版のソルバでは、求解アルゴリズムを一つ追加したのでその結果も合わせて載せております。

MaxSAT Competition 2017にエントリしました。

今年から、大分ルールが変わったようです。

まずオーガナイザが、現役のトップアスリートになったようです。MachineがStarExeClusterというSAT　Competitionでも共用するClusteringMachineになりました。１Instanceあたりのメモリが２４GB、MainTrackの制限時間が１時間という仕様に代わりました。
　MainTrackでは、StateOfArtのソルバがひしめきます。こちらはAcademicな観点からMaxSATの主戦場でしょう。対して、NSP(NurseSchedulingProblem)は、実質的な解をReasonableな時間内に得ることが主眼であって必ずしも厳密解にはこだわりません。そのため、InCompleteTrackで出場することにしました。こちらは、６０secまたは、300sec内となっており、実際の現場での仕様状態に近いものです。
今回は、アナウンスから締め切り（6/15)が極端に短いので、逆に有利かもしれません。まだ、11組しかおりませんでしたし。

ともあれ、NSPのCompetitionでもそうでしたが、ソルバを作ってチューニングをするのは、子どものころのプラモデルを作る楽しみに似て、心躍るものがあります。
　Clustering上でテストもできるようなので、そのうちテストしてみたいと思います。

独占ライセンス契約を締結しました。

締結先は、マルマンコンピュータサービス株式会社です。

ソルバ（求解エンジン）の独占ライセンスですので、スケジュールナースには何等影響がなく、これまでどおり販売・サポートしていきます。

スケジュールナースⅡリリース

GUIを全面的に書き直しました。
英語と日本語に対応しました。

DataGridは、syncfusion　windows.formsを有り難く使わせて頂いております。
GUIについては、ソルバの使い方の説明としてのDoxygen生成VisualStudioC#ソースコードです。

マニュアルはこちらです。

スケジュールナース 外部サーバ廃止

匠シフタ（モバイル用）のリリースに伴い、スケジュールナースの外部サーバは廃止になりました。

旧バージョンをお使いの方は、「外部サーバ使用」のチェックを外してお使いください。