Solving Linear Optimization Problems for Pseudo-Booleans and Yonder

の略らしいです。ワークショップです。

確かに、SATを一般のMIP問題に適用しようとすると、CNF表現では、無理があると思います。これを疑似ブーリアンと抽象化することで、IP問題と親和性が生まれます。で、そこにCutting Proofを入れるという発想は自然なものとなります。

ただし、一般にLPの速度は、CDCLのバックトラックに比べ、二けた以上遅いので毎回行う訳には行きません。LPソルバを導入した場合、この辺をどうバランスを取っていくかというのが実装上の問題かと思います。