SAT Part 2 — Arithmetic

This is the second part of the SAT series. For your convenience you can find other parts in the table of contents in Part 1 — Boolean logic

Today we’re going to implement some basic arithmetic in SAT.


We assume numbers are represented using U2 scheme. All we need to do is to implement a full-adder. We can use the following code (it comes from my custom SAT solver for MilpManager wrapper):

Let’s unwrap this magic one by one.

First, in line 3 we create a variable for holding the result. We assume it creates enough clauses for integer.

Next, we clear previous carry index (the input to the full adder).

In lines 8-29 we implement a loop which adds bits one by one. We create a new carry in line 13 and then calculate it by using conjunction.

Next, in line 17 we calculate the half-add by xoring bits.

Next, we need to propagate carry properly. In lines 23-26 we do the math.


Negation is very simple. First, we negate all bits, and then we add one (using the addition scheme from previous section).


Super simple, just add negated number.


We’re going to cheat a little. Since we represent numbers with fixed number of bits, we can ignore the overflow and just do the long multiplication, like this: