又一种At-Most-K约束的SAT编码比较
计算机科学中的逻辑
2020-05-14 v1 人工智能
摘要
at-most-k约束在组合问题中无处不在，且该约束有众多SAT编码可用。先前的实验已显示序列计数器编码在k 1时的竞争力，并因并行计数器编码无法通过单元传播强制弧一致性，将其排除在考量之外——而它比二进制加法器编码更紧凑。本文给出一个实验，展示了二进制加法器编码用于at-most-k约束时的惊人性能。
引用
@article{arxiv.2005.06274,
title = {Yet Another Comparison of SAT Encodings for the At-Most-K Constraint},
author = {Neng-Fa Zhou},
journal= {arXiv preprint arXiv:2005.06274},
year = {2020}
}