提出 Ladder AMK 约束的新型 SAT 编码

论文提出一种针对 Ladder 结构 At-Most-K 约束的新型 SAT 编码。该方法将约束序列分解为独立块并整体编码，使用 Sequential Counter 和连接子句，相比基于 BDD 的编码减少了变量数和子句数。实验表明该方法在解决 Anti-bandwidth 和 Nurse Rostering 问题时，效率优于现有编码及更高级的约束规划求解器。