z3 - Gurobi 可以用来解决 SMT-LIB 文件吗？

Question

我有一个问题，我们之前使用混合整数线性规划 (MILP) 和 Gurobi 解决了这个问题。问题空间涉及大约 2 亿个整数变量，其中除了 5000 之外的所有变量都是零，而 5000（一个非常具体的 5000）是 1。唯一的算术是加法。

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

我已将问题重新编码到 SMT-LIB 中。现在问题要小得多——只有 100,000 个整数变量。现在使用的函数是ite和+和。但在非常简单的问题上，Z3 的耗时大约比 Gurobi 长 10 到 100 倍。=assert

有什么方法可以让 Gurobi 处理 SMT-LIB 文件？

编辑：我没有优化，我只对找到令人满意的解决方案感兴趣。

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

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

标签： z3smtgurobi