Branchingだけで整数解を出すことは可能か？

答えは、Yesです。

SATソルバを使わずにBranchingだけで、整数解を得ることは可能です。逆の場合、LpSolverBranchingを使わずにROOTでSAT　Solveする試みは失敗しました。つまり、

LpSolverBranching＞SAT Solver

であることは、前回までの実験で明らかとなりました。

一言で言うならば、この違いは、アナログ値を扱うか？ということに尽きます。Branchingでは、基本的にFractionalな点でBranchingしていきます。Branching前、Fractionals数は最大です。この時点においてもLpSolverでは、0/1 Fixed Litsは存在することがポイントです。この時点のFixed Litsは、リニア空間上のFixed Litsですから、整数解におけるそれとは違います。違いますが、一般には、近い関係にあります。つまり、Branchingする前からしてある程度、固定でないビット(Fractional)は、限定されている、ということが言えます。SAT Solverでは、このアナログ的な概念がないので、やみくもに探索空間をFULLに０/1を割り当てて（Decision）最後まで割り当てられるかをカットアンドトライをひたすら繰り返すのが違います。当然それが効くのは、ある程度探索空間が絞られた状態に限ります。

下記の値は、SAT SOLVE techniqueを使わないで、整数解を求めるまでの時間を示しています。もちろん、数々のOR techniqueは駆使していますが、最も大きな効果はBranchingによるものです。

Instance21でのDepth-Fractionalsグラフです。整数解に達するまで、およそ5000Branchを要しています。最終的な目的関数値には、およそ3500Depthで21333に到達しています。

インスタンス21に関しては、およそ50000secで、Optimum整数解はでますが、Instance24の規模は、このおよそ12倍の規模になります。LPSolverの行規模で言うとおよそ3倍近くになります。BarrierSolverは、行規模のおよそ3乗で効いてくるのでとても遅くなるのがネックになっています。現状では、およそ40日廻さないとFractionalsは、ゼロになってくれない見通しです。

そこで、二つのアプローチを考えました。

一つ目のアイデアは、fullに探索空間を探すことに無理があるので、いきなりSATSolveせずに、MaxSAT的アプローチで、限定した探索空間にすることです。そうすることにより、SAT解の出やすいところので、学習項が出やすくなるであろう、と期待されます。しかし、それが、効き始めるまでは、やはりかなり限定した空間になっている必要があり、それまでの間かなり長い時間を要してしまいます。結局は、補助的な手段にしか、なり得ないでしょう。

2番目のアイデアは、行そのものを削除していくアイデアです。これであれば、最初は、遅くとも、Branchが進めば進むほど、速度アップが期待できます。