UBを表すMDD Structure

 SAT Solverは、MDDを採用します。SchedulingBenchmarksにおいて、重みは、わずか4種類に限定されます。100,3,2,1です。100は、UnderStaffingです。１は、OverStaffingの重みと希望休みの重みとで共用しています。

これをMDD構造で書くと

という具体になります。大きな重み順にTreeを構成した方がノード数が少なくて済みます。最終的なTarget UB Nodeは、一つに限られます。Nodeから出るEdgeは、重み係数です。各々の重みは、UnaryCounterによって構成されています。例えば、最初の階層34700を実現するには、347の値を指しているUnaryCounterをEncodeすればよいです。

このTreeの大きさを決めるのは、各重み係数のあり得る範囲に依存します。この範囲が狭ければ狭い程、探索Treeを小さくできるので、高速にSAT/UNSAT解が求まることになります。

MDDがやっていることは、

■TargetUBになり得るすべての重み係数の組み合わせを列挙する

ということだけです。

＜Treeをなるべく小さくするには＞

■重い順から列挙

■係数範囲を絞る

当然、重み種類が多ければ多い程、また係数範囲が大きければ大きい程、Tree大きくなり、最悪の場合爆発、破綻します。そこで、あり得る範囲を限定する作業が必要になってきます。

各重み係数範囲を理論的に求めるのは、OR手法を用いて行いますが、かなり高度です。ここでは、それが求まっていることを前提に話を進めます。

＜UnaryCounterとは＞

UnaryCounterは、1進カウンタです。定番のEncodingです。SATSolverに乗せるには、必須のテクニックですが、数々の方法が提案されています。これ位の規模だとTotalizer一択です。