Constraint Solving for Interpolation https://www7.in.tum.de/~rybal/papers/jsc-2010-constraint-solving-for-interpolation.pdf LRAとLRA∪EUFにおけるクレイグ補間の生成アルゴリズム。 タイトルからMUS列挙のような組み合わせの探索の話かと思ったら、Farkasの補題的な感じでLRAに帰着する感じだった。 LRA∪EUFの場合は工夫した Ackermann's expansion でLRAの場合に帰着？ (あまりちゃんと読めてないけれど)