许多论文都在使用 SAT，但很少有人提到如何将附加项转换为 CNF。
由于 CNF 只允许 AND OR 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. Encoding Linear Constraints with Implication Chains to CNF，2. SAT-Based Techniques for Integer Linear Constraints。这可能会有所帮助。