我有一个问题，我们以前使用混合整数线性程序（MILP）和Gurobi来解决。问题空间涉及大约2亿个整数变量，除5000之外的所有变量均为零，而5000（非常具体的5000）为1。唯一的算法就是加法。

用于此问题的Gurobi输入文件的大小通常为5-10GB（太大，以至于我将它们压缩存储并开发了一个gurobi hack来读取gzip格式的文件）。 Gurobi通常可以在60-600秒内解决这些问题，但有时可以在6000秒内解决。甚至六万永远不要60万。

我已将问题重新编码为SMT-LIB。现在的问题要小得多-仅有100,000个整数变量。现在使用的功能是ite和+以及=和assert。但是在一些简单的问题上，Z3花费的时间比Gurobi长10到100倍。

有没有办法让Gurobi处理SMT-LIB文件？

编辑：我不是在优化，我只是想找到令人满意的解决方案。

顺便说一句，我应该看看其他求解器吗？

另一方面，我怀疑将问题从100,000,000整数更改为100,000会使问题更难解决。这两个问题之间的映射是，大问题sin的整数变量聚集在大约15,000的组中，而在小问题中，我却有一个8位数字，一个6位数字和两个1位数字） 。也许我应该给Z3更大的问题？