我正试图用一个解决一个大的CNF公式SAT solver.公式(DIMACS格式)有4,697,898,048 = 2^32 + 402,930,752条款,我找到的所有SAT求解器都有问题:
- (P)lingeling报告"有太多条款"(即比标题行指定的条款更多,但事实并非如此)
- CryptoMiniSat4和picosat宣称读取标题行为402,930,752条款,其中2 ^ 32太少
- 葡萄糖似乎解析了98,916,961条款,然后报告使用简化解决了UNSAT公式,但这不太可能是正确的(公式的初始部分很短很可能是SAT).
是否有人知道可以处理这么大的文件的SAT求解器？或者是否有类似编译器开关的东西可以回避这种行为？我相信所有求解器都是为64位linux编译的.(当谈到处理这么大的数字时,我有点像菜鸟.抱歉.)