新しい整数化フェーズ方法

 LpsolverでLBを求めたあと、Branchとヒューリスティックを用いて整数化を行うのが常道です。しかしながら、Instance24は、超巨大インスタンスであり、常道のBranchを行って整数化を行っていたのでは、途方もない時間がかかってしまいます。そこで、新しい整数化方法を考えました。

上が、その系で、BranchしないIteration Loopになっています。TargetUB＝ceil(LB)を選び、

LP SolverとSAT Solverとの間で通信をしながら、徐々にBITを固定化していきます。めでたくSAT解が得られれば、そこで終了です。UNSATもしくは、LpSolverのLBが、TargetUBを超えたら、TargetUBはUNSATという証明が得られたということです。TargetUB+=1にしてIteration Loopをやり直します。この系においてはBranchingしないことが特徴です。Branchingするということは、その裏も厳密性のためには結局は見ないといけないです。ヒューリスティックにBranchしていたのでは、UNSATの厳密性が得られません。あくまで、厳密解にこだわったループになっています。

この方式は、MAXSATでは一般的なUNSAT 解法を模していますが、Lp Solverを含めたところが新しいです。多くの場合SATSolverがUNSATを返すよりも、LPSolverがExcessiveLBを検出する方が早いだろう、と予測しています。

一般的にSATSolverで、OR問題を解いたとき、UNSATを返すのは、UNSATLOOP初期段階もしくは、軽い系に限られることが多いです。真のBoundary付近では、SAT/UNSATの判別がつかない、という場面を多く経験しました。それに対してLP　SolverとSAT　Solverが互いに助けながら学習を進めていくこの方式は、互いの強みを生かしながら同時に弱点を補完しあいます。LPとSAT,アナログとデジタルのHybridループになっています。SATSOLVERは、UNSATを証明するための濃厚かつ重厚緻密計算を行う必要はないだろう、と見ています。

実は、Instance15を解いたときに、多くのBranchingLOOPを廻しました。計算機を一週間近く廻さないと、そのLBでは解がない、UNSAT証明が出来ませんでした。こうした場面でも上記アプローチは、有効ではないかと期待されます。

この方式では、目的関数値がLB近傍にあるときBranchingよりも高速に整数化できると期待されます。また上手くいったら、市井のNSPに対しても本方式を採用したいと思っています。