c - SAT 求解超过 2^32 个子句

Question

我正在尝试使用SAT solver. 公式（DIMACS格式）有4,697,898,048 = 2^32 + 402,930,752子句，我能找到的所有 SAT 求解器都遇到了问题：

• (P)lingeling报告“子句太多”（即子句比标题行指定的多，但事实并非如此）
• CryptoMiniSat4 & picosat声称读取标题行时说 402,930,752 个子句太少了 2^32
• Glucose似乎解析了 98,916,961 个子句，然后报告已使用简化将公式求解为 UNSAT，但这不太可能是正确的（公式的初始部分很可能是 SAT）。

有人知道可以处理这么大文件的 SAT 求解器吗？或者是否有类似编译器开关的东西可以回避这种行为？我相信所有求解器都是为64bit linux编译的。（在处理这么大的数字时，我有点菜鸟，抱歉。）

Answer 1

我是 CryptoMiniSat 的开发者。在 CNF 如此庞大的大多数情况下，问题不在于 SAT 求解器，而是原始问题到 CNF 的转换做得不够仔细。我假设您没有手动编写 CNF——您遇到了一个问题，您使用自动化工具将其转换为 CNF。

将问题转换为 CNF 的行为称为编码，它在学术界有大量文献。它本身就是一个完整的话题，或者更恰当地说，它本身就是一个完整的话题。请参阅有关约束编程 (CP)、伪布尔约束 (PB)、ANF 到 CNF 转换技术（参见 crypo 研讨会/会议）和电子电路编码（搜索 AIG、Tseitin 编码及其变体）的研究论文并查看在参考文献）。这些是大话题，但还有很多其他话题。看看这些将使您的 CNF 减少至少 3 个数量级，可能更多。