我一直在使用 MAX-SAT 求解器来获得 ising 旋转玻璃模型的确切基态：

对于一维周期模型，对于具有 50 个二元变量和第 15 个最近邻的交互范围的系统。最好的 MAX-sat 求解器需要 20 分钟才能求解。对于 100 个二进制文件，它变得不可能......

然而，当人们使用图论最大割方法来解决这个问题时，他们似乎可以获得更大规模的基态。但是我想知道如果我将我的 ising spin glass 问题转换为图形切割的格式，图形切割求解器会以任何方式更好地执行吗？为 maxsat 构造定理的人是否不考虑其图割等效方法？为了您的兴趣，我的 50/100 变量问题的情况如下：

https://www.dropbox.com/s/23lo7lwgd4otse9/50_softer.wcnf?dl=0 https://www.dropbox.com/s/r2r1yfpb2uzvcrn/100_softer.wcnf?dl=0

（您可能会看到有 64、114 个变量，但硬约束强制前 15 个子句与后 15 个子句相等）

供您参考，在大多数情况下，求解器可以快速找到确切的基态，但证明过程非常缓慢（例如，需要 1 秒才能获得真正的解决方案，而使用 20 分钟来证明）...