拆分和/或分区大型CNF文件/矩阵

Question

简单的问题。我有一个非常大的CNF文件，它代表一个mxn矩阵。假设>；10000个变量和相关术语。因此，作为第一步，我想对CNF文件进行分区，或者更好地将矩阵分解为100个变量，以便并行求解概念。有什么说明适用什么规则吗？在

感谢所有的帮助。在

问候 阿德里安

Answer 1

您可以使用graph partitioning工具，如Metis将CNF子句聚集到不共享任何变量的独立集中。在

如果无法识别真正断开连接的集群，那么“链接变量”的数量可能会小到足以枚举它们的值。这样的枚举基本上为连接的变量分配一个暂定值，并在搜索过程中消除它们。要付出的代价是，您必须对每个值组合运行搜索。在

现代SAT求解器如Cryptominisat、Riss3g或Lingeling应用各种预处理措施来减小问题的规模。然而，10000个变量可能是一个可行的大小，不需要额外的步骤就可以解决。在

单是CNF的大小并不是可靠的指标，也不能说明问题的复杂性。Tseitin encoding是一种常用于减少CNF中子句数的技术。在

正如在this post中推荐的那样：一篇包含大量关于SAT编码工作的有用参考文献的好论文是Magnus Björk于2009年7月25日撰写的“成功的SAT编码技术”： http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf