基于比较器网络的基数约束CNF编码

布尔可满足性问题（SAT）是计算机科学的核心问题之一。作为基本的NP完全问题之一，通过已知的归约，它可用于表示各种困难决策问题的实例。此外，这些表示可交由寻找布尔公式满足赋值的程序处理，例如名为 MiniSat 的程序。这些程序（称为 SAT 求解器）已被深入研发多年，并且——尽管具有最坏情形指数时间复杂度——能够求解大量困难的实际实例。该方法的一个缺陷是子句既无表现力也不紧凑，用它们描述决策问题本身可能构成巨大挑战。我们可以通过使用高层约束作为手头问题与 SAT 之间的桥梁来改进这一点。此类约束随后被自动翻译为等可满足的布尔公式。本论文的主题围绕一类此类约束展开，即布尔基数约束（或简称基数约束）。基数约束表述为 $n$ 个命题文字中至多（至少，或恰好）$k$ 个可以为真。此类基数约束自然地出现在各类现实问题的表述中，包括累积调度、时间表排布或形式化硬件验证。本论文的目标是提出并分析将基数约束编码（翻译）为 CNF 中等可满足命题公式的新的高效方法，使得所得 SAT 实例规模小且 SAT 求解器运行时间尽可能短。