UNSAT APPROACH

 MAXSATのアプローチの仕方としては、SATから攻める方法と、UNSATから積み上げていく方法があります。

基本的にスケジュールナースのAL1で使っているのは、上のSAT Approachになります。厳密解かどうかは、現在の目的関数値未満の値がUNSATとなることによって初めて、判明します。現在の目的関数値を下回る解が存在しない(UNSAT)を示すことに必要となるので、このハードルは、極めて高いです。ある目的関数値が示すことであれば、その1点だけに注力すればよいのですが、あらゆるケースにおいて存在しないことを示さないとUNSATとは言えないからです。

一方UNSAT approachは、Fu & Malikによって開発されたアルゴリズムで、UNSATを下から積み上げてゆく方式で、SATになったときに厳密解となります。

この方法は、前述のassumptionを用いることが必須です。この方式の難点は、UNSATのまま停滞することが多く、SAT解がえられないまま終わることが多い、つまり解が得られないまま終わる、ということです。スケジュールナースの実務インスタンスで言えば、ほとんどエラーのないインスタンスのみしか適用することが出来ないので、効果的な場面は存在するものの、汎用的ではありません。

残念なことに、kissatが、incremental/assumptionの実装を放棄した関係で、MAXSAT関係では、最新SATソルバの恩恵を得ることが出来ずに、最近の進歩は停滞しています。