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

Question

我正在尝试使用 SAT 求解器 求解大型 CNF 公式。公式(DIMACS 格式)有 4,697,898,048 = 2^32 + 402,930,752 子句，我能找到的所有 SAT 求解器都遇到了问题:

• (P)lingeling reports that there are "too many clauses" (i.e. more clauses than the header line specifies, but this is not the case)
• CryptoMiniSat4 & picosat claim to read the header line as saying 402,930,752 clauses which are 2^32 too few
• Glucose seems to parse 98,916,961 clauses and then reports to have solved the formula as UNSAT using simplification, but this is unlikely to be correct (an initial segment of the formula this short is very likely to be SAT).

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

Answer 1

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

将问题转化为 CNF 的行为称为编码，它在学术界有大量文献。它本身就是一个完整的话题，或者更恰本地说，是它们自己的整个话题。请参阅有关约束编程 (CP)、伪 bool 约束 (PB)、ANF-to-CNF 转换技术(参见 crypo 研讨会/ session )和电子电路编码(搜索 AIG、Tseitin 编码及其变体并查看在引用)。这些都是大话题，但还有很多其他话题。看一眼这些就会将你的 CNF 降低至少 3 个数量级，可能更多。