How to using CNFs to describe addition

Question

Many papers are using SAT, but few mentioned how to convert an addition to CNF.

Since CNF only allows AND OR NOT operation, it is difficult to describe addition operation. For example,

x1 + x2 + x3 + ... +x1599 < 30, xi is binary.

1. Map these equations into a Boolean circuit.
2. Apply Tseitin's transformation to the circuit and convert it into DIMACS format.

But is there any way to read the results? I do think it is possible to read the results if all the variables are defined by ourself, so figuring out how to convert a linear constraint to SAT problem is necessary.

If there are 3 or 4 variables, i.e. x1+x2+x3 <3, we can use truth table to solve this conversion. Also, a direct way is that chose 29 (any number smaller than 30) variables from 1600 variables to be 1, the others to be 0. But there are too many possibilities which makes this problem hard to solve.

I have used STP, but it can only give 1 answer. As the increasing number of variables and clauses, it costs a long time for STP to run.

So I tried to use SAT to solve the cnf given by STP, it can give out answers in a minutes. But the results cannot be read.

In the end, I found some paper, 1. Encoding Linear Constraints with Implication Chains to CNF, 2. SAT-Based Techniques for Integer Linear Constraints. This may be helpful.

Answer 1

What you're describing is known as a cardinality constraint. There are many ways of encoding these in CNF. As a starting point, some of these encodings are explained in

• http://www.carstensinz.de/papers/CP-2005.pdf and
• https://arxiv.org/pdf/1012.3853.pdf.

Many are implemented in the PySAT python toolkit

• https://pysathq.github.io/docs/html/api/card.html