Algorithm5の時間定義の変更

 今まで、時間は、そのままの定義でしたが、Algorithm5では、時間の定義を変えています。今までは、高性能PCの１０秒と、低性能PCの１０秒では、目的関数値の値が変わることはありました。しかし、１０秒は１０秒でどちらも同じです。Algorithm５では、それが変わります。

ソルバを決定的にするには、Decision数もしくは、Conflict数をLimitにする必要があります。Decisionというのは、変数に「えいや！」と当てずっぽうで０か１に割り当てることです。全ての変数を矛盾なく割り当てられたときに解があります。当てずっぽうなので、大抵どこかで矛盾が生じます。矛盾が生じたら、問題となる原因のところまで戻って変数の割り当てをやり直します。戻ることをバックトラック、矛盾が生じたことをConflictと呼びます。

基本的には、Decision数と秒の関係を一定とみなして、対応するDecision数をLimitにします。そうすると、いわばClock数でLimitにすることに対応するので、遅いPCと速いPCでは、実行時間に差が生じることになります。しかし、どちらも同じ目的関数値になることが期待できることになります。

残念ながら、Decision数と時間との関係は一定ではなく最大で２０倍程度の差があることが分かっています。なので、あまりにも目標の時間に到達していない場合は、積み増ししてなるべく目標時間になるような実装としました。その結果として、必ずしも決定的にはなりません。しかし、プロジェクトファイルが同じならば、時間のかかり具合はPCで変わろうとも、ほぼ同じ結果となることが期待できます。