Detecting Cardinality Constraints in CNF
Detecting Cardinality Constraints in CNF
复制标题
检测 CNF 中的基数约束
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Norbert Manthey
中科院分区：
文献类型：
--
作者：
Armin Biere;Daniel Le Berre;Emmanuel Lonca;Norbert Manthey
我们提出了新的方法来检测以CNF表示的基数约束。第一种方法是基于对SAT求解器中用来表示二进制子句和三进制子句的特定数据结构的句法分析，而第二种方法是基于单位传播的语义分析。语法方法非常快速地计算基数约束AtMost-1和AtMost-2的近似值，而语义方法具有通用性，即它可以以较高的计算代价检测任意k的基数约束AtMost-k。实验结果表明，这两种方法在恢复AtMost-1和AtMost-2基数约束方面都是有效的。
We present novel approaches to detect cardinality constraints expressed in CNF. The first approach is based on a syntactic analysis of specific data structures used in SAT solvers to represent binary and ternary clauses, whereas the second approach is based on a semantic analysis by unit propagation. The syntactic approach computes an approximation of the cardinality constraints AtMost-1 and AtMost-2 constraints very fast, whereas the semantic approach has the property to be generic, i.e. it can detect cardinality constraints AtMost-k for any k, at a higher computation cost. Our experimental results suggest that both approaches are efficient at recovering AtMost-1 and AtMost-2 cardinality constraints.