Yet Another Comparison of SAT Encodings for the At-Most-K Constraint
Logic in Computer Science
2020-05-14 v1 Artificial Intelligence
Abstract
The at-most-k constraint is ubiquitous in combinatorial problems, and numerous SAT encodings are available for the constraint. Prior experiments have shown the competitiveness of the sequential-counter encoding for k 1, and have excluded the parallel-counter encoding, which is more compact that the binary-adder encoding, from consideration due to its incapability of enforcing arc consistency through unit propagation. This paper presents an experiment that shows astounding performance of the binary-adder encoding for the at-most-k constraint.
Keywords
Cite
@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}
}