KCNF公式

合取范式（CNF）的带计数约束变体，每个子句附带关于真实文字数量的精确约束，常用于研究计数复杂性的精细结构。