# Yet Another Comparison of SAT Encodings for the At-Most-K Constraint

arXiv: https://arxiv.org/abs/2005.06274 · HTML: https://mlsanity.com/paper/2005.06274/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 May 2020.

## Built on by (most cited first, 1 of 1)

- [Asymptotically Smaller Encodings for Graph Problems and Scheduling](https://mlsanity.com/paper/2506.14042/) (2025)

## Abstract (arXiv)

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.