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

TL;DR

This paper compares various SAT encodings for the at-most-k constraint, revealing unexpectedly superior performance of the binary-adder encoding, challenging previous assumptions about encoding efficiency and arc consistency enforcement.

Contribution

It provides the first comprehensive experimental comparison including the binary-adder encoding, demonstrating its competitive performance for at-most-k constraints.

Findings

Binary-adder encoding outperforms other encodings in experiments

Sequential-counter encoding remains competitive for k > 1

Parallel-counter encoding's limitations are confirmed

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.