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

2020/05/12 by Neng‐Fa Zhou, Zhou, Neng-Fa · 1 citation
Computer Science · #Algorithms and Data Compression #Artificial Intelligence (cs.AI) #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO)

paper · pdf · doi:10.48550/arxiv.2005.06274

openalex publication_date 2020/05/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Asymptotically Smaller Encodings for Graph Problems and Scheduling

Related

• A comparison of encodings for cardinality constraints in a SAT solver
• Approximate-At-Most-k Encoding of SAT for Soft Constraints
• Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT
• A Simpler Exponential-Time Approximation Algorithm for MAX-k-SAT
• Encoding Linear Constraints into SAT