In the field of Boolean satisfiability problems (SAT), at-most-k constraints, which suppress the number of true target variables at most k, are often used to describe objective problems. At-most-k constraints are used not only for absolutely necessary constraints (hard constraints) but also for challenging constraints (soft constraints) to search for better solutions. To encode at-most-k constraints into Boolean expressions, there is a problem that the number of Boolean expressions basically increases exponentially with the number of target variables, so at-most-k often has difficulties for a large number of variables. To solve this problem, this paper proposes a new encoding method of at-most-k constraints, called approximate-at-most-k, which has totally fewer Boolean expressions than conventional methods on the one hand. On the other hand, it has lost completeness, i.e., some Boolean value assignments that satisfy the original at-most-k are not allowed with approximate-at-most-k; hence, it is called approximate. Without completeness, we still have potential benefits by using them only as soft constraints. For example, approximate-at-most-16 out of 32 variables requires only 15% of a conventional at-most-k on the literal number and covers 44% of the solution space. Thus, approximate-at-most-k can become an alternative encoding method for at-most-k, especially as soft constraints.

翻译：在布尔可满足性问题（SAT）领域中，最多-k约束（用于限制真值目标变量数量不超过k）常用于描述目标问题。最多-k约束不仅用于绝对必要约束（硬约束），也用于挑战性约束（软约束）以搜索更优解。将最多-k约束编码为布尔表达式时存在一个难题：布尔表达式数量基本随目标变量数量呈指数增长，因此对于大量变量问题，最多-k约束常面临困难。为解决此问题，本文提出一种称为近似最多-k的新型最多-k约束编码方法，其布尔表达式总量显著少于传统方法。但该方法牺牲了完备性，即某些满足原始最多-k约束的布尔赋值在近似最多-k中不被允许，故称为"近似"。尽管缺乏完备性，将其仅作为软约束使用时仍具有潜在优势。例如，在32个变量中取16个变量的近似最多-k约束，其文字数量仅为传统最多-k约束的15%，却能覆盖44%的解空间。因此，近似最多-k可成为最多-k约束的替代编码方案，尤其适用于软约束场景。