ILP Modulo Theories http://www.ccs.neu.edu/home/vpap/pub/cav-2013.pdf SMTのSAT部分をILPに置き換えて、整数線形算術∪T のセオリー上の最適化問題を解く。 Tに関する推論を含めた Branch-and-Cut のアルゴリズム BC(T) が、DPLL(T)スタイルの遷移規則で書かれていて、なるほどという感じ。
Cutting to the Chase http://csl.sri.com/users/dejan/papers/jovanovic-cade2011.pdf が、SATのCDCLを整数線形算術に一般化していたのに対して、こっちは整数線形算術（整数線形計画）のアルゴリズムをSAT/SMTのCDCL部分の置き換えに持ってきていて、対照的で面白い。
評価はちょっと微妙かも。 Boeing 787 のアーキテクチャ合成の問題で、SMTソルバのZ3やMathSATと、MIPソルバのCPLEXやSCIPなどと比較して、IMT Modulo Theories (IMT) アプローチの必要性を言っているのだけど、実装したInezはSMT_LIBの QF_UFLIA (Quantifier-Free Linear Integer Arithmetic with Uninterpreted Functions) での評価ではSMTソルバに勝てておらず、アーキテクチャ合成の問題でも、通常のSMTソルバやMIPソルバを使う場合と比べてどうだったのかが書かれていなかったので、結局のところどうなのかが良くわからない。
CoBaSA
http://www.ccs.neu.edu/home/pete/cobasa.html
Inez
https://github.com/jpais/inez