最近のニュースレター記事で、私は研究者が自分の研究の適用可能性について誤解を招く方法について不満を述べました。SATソルバーを例として挙げました。人々は興味深い例を返信してくれたのですが、私にとって新しいものだったのは、SATの拡張であるSMT(Satisfiability Modulo Theories)の概念でした。SMTは、vanilla SATよりも実用的応用が多いようです(詳細はニュースレターを参照してください)。
SMTソルバーを調べてみる時間を取ったかったので、MicrosoftのオープンソースSMTソルバーであるZ3にたどり着きました。
jeremykun.com
Optimization Models for Subset Cover
Create attached notes ...
