简单的问题。我有一个非常大的 CNF 文件，它代表一个 mxn 矩阵。可以说具有相关术语的 >10000 个变量。因此，作为第一步，我想对 CNF 文件进行分区，或者甚至更好地将矩阵拆分为 100 个变量以用于并行求解概念。有没有说明适用什么规则？
感谢所有帮助。
问候阿德里安
问问题
242 次
1 回答
1
您可以使用像Metis这样的图形分区工具将子句聚集成不共享任何变量的独立集合。CNF
如果无法识别真正断开的集群，则“链接变量”的数量可能足够小以枚举它们的值。这种枚举基本上为连接变量分配一个暂定值，并在搜索过程中消除它们。要付出的代价是您必须对每个值组合进行搜索。
现代 SAT 求解器，如Cryptominisat、Riss3g或Lingeling ，采用各种预处理措施来缩小问题的规模。但是，10000 个变量可能是无需额外步骤即可解决的可行大小。
单独的 CNF 大小不是可靠的指标或问题的复杂性。Tseitin 编码是一种经常用于减少 CNF 中子句数量的技术。
正如这篇文章中所推荐的：一篇不错的论文，其中包含很多关于 SAT 编码工作的有用参考，是 Magnus Björk 的“成功的 SAT 编码技术”，2009 年 7 月 25 日：http: //jsat.ewi.tudelft.nl/addendum/ Bjork_encoding.pdf </p>
于 2014-04-08T09:06:48.803 回答