许多论文都在使用SAT，但很少有人提到如何将加法转换为CNF。
由于CNF只允许AND或NOT操作，因此很难描述加法操作。例如
x1 + x2 + x3 + ... +x1599 < 30, xi is binary.
- 将这些方程映射到布尔电路中。
- 将 Tseitin 的变换应用于电路并将其转换为 DIMACS 格式。
但是有什么方法可以读取结果吗？我确实认为，如果所有变量都由我们自己定义，则可以读取结果，因此弄清楚如何将线性约束转换为SAT问题是必要的。
如果有 3 或 4 个变量，即 x1+x2+x3 <3，我们可以使用真值表来解决此转换。此外，一种直接的方法是从 1600 个变量中选择 29 个(任何小于 30 的数字(变量为 1，其他变量为 0。但是有太多的可能性使这个问题难以解决。
我使用过STP，但它只能给出1个答案。随着变量和子句数量的不断增加，STP 的运行需要很长时间。
所以我试着用SAT来解决STP给出的cnf，它可以在几分钟内给出答案。但结果无法读取。
最后，我找到了一些纸， 1. 将带有隐含链的线性约束编码为 CNF， 2. 基于SAT的整数线性约束技术。这可能会有所帮助。
您所描述的称为基数约束。在 CNF 中编码这些内容的方法有很多种。作为起点，其中一些编码在
- http://www.carstensinz.de/papers/CP-2005.pdf 和
- https://arxiv.org/pdf/1012.3853.pdf。
许多是在PySAT python工具包中实现
的- https://pysathq.github.io/docs/html/api/card.html