Verified Solutions to Integer Programming Problems (Daniel Steffy): https://github.com/ambros-gleixner/VIPR の話。 個人的にはDRAT-trimをresolutionからcutting-plane proof systemへ一般化するようなアプローチとの類似や違いが気になった。 あと、生成されるcertificateは数百GBくらいのようで、SATで200TBとか言っていたの https://plus.google.com/+MasahiroSakai/posts/dddK6XDk2A3 とくらべるとだいぶ小さな気はして、単に実験した問題が小さかったのか、本質的に小さくなる理由があるのかも、ちょっと気になった。