Let's solve the following equation $a+b=4 \equiv 2^4$ on the 4-bit CPU (hence, modulo $2^4$):

(declare-fun a () (_ BitVec 4))
(declare-fun b () (_ BitVec 4))

(assert (= (bvadd a b) #x4))

; find a, b:
(get-all-models)



There are 16 possible solutions (easy to check):

(model
(define-fun a () (_ BitVec 4) (_ bv0 4)) ; 0x0
(define-fun b () (_ BitVec 4) (_ bv4 4)) ; 0x4
)
(model
(define-fun a () (_ BitVec 4) (_ bv12 4)) ; 0xc
(define-fun b () (_ BitVec 4) (_ bv8 4)) ; 0x8
)

...

(model
(define-fun a () (_ BitVec 4) (_ bv9 4)) ; 0x9
(define-fun b () (_ BitVec 4) (_ bv11 4)) ; 0xb
)
Model count: 16


How I implemented this in my toy-level SMT solver?

First, we need an electronic adder, like it's implemented in digital circuits. This is basic block (full-adder) (image taken from Wikipeda):

This is how full adders gathered together to form a simple 4-bit carry-ripple adder (also from Wikipedia):

void add_Tseitin_XOR(int v1, int v2, int v3)
{
add_comment ("%s %d=%d^%d", __FUNCTION__, v3, v1, v2);
};

void add_Tseitin_OR2(int v1, int v2, int var_out)
{
add_comment ("%s %d=%d|%d", __FUNCTION__, var_out, v1, v2);
add_clause("%d %d -%d", v1, v2, var_out);
};

void add_Tseitin_AND(int a, int b, int out)
{
add_comment ("%s %d=%d&%d", __FUNCTION__, out, a, b);
};

void add_FA(int a, int b, int cin, int s, int cout)
{
add_comment("%s inputs=%d, %d, cin=%d, s=%d, cout=%d", __FUNCTION__, a, b, cin, s, cout);
// allocate 3 "joint" variables:
int XOR1_out=next_var_no++;
int AND1_out=next_var_no++;
int AND2_out=next_var_no++;
// add gates and connect them.
// order doesn't matter, BTW:
};


add_Tseitin* functions makes logic gates in CNF form: https://en.wikipedia.org/wiki/Tseytin_transformation. Then I connect logic gates to make full-adder.

void generate_adder(struct variable* a, struct variable* b, struct variable *carry_in, // inputs
struct variable** sum, struct variable** carry_out) // outputs
{

...

int carry=carry_in->var_no;

// the first full-adder could be half-adder, but we make things simple here
for (int i=0; iwidth; i++)
{
// newly created carry_out is a carry_in for the next full-adder:
carry=(*carry_out)->var_no;
};
};


Let's take a look on output CNF file:

p cnf 40 114
c always false
-1 0
c always true
2 0
c add_FA inputs=3, 7, cin=1, s=11, cout=15
-3 -7 -16 0
3 7 -16 0
3 -7 16 0
-3 7 16 0
-16 -1 -11 0
16 1 -11 0
16 -1 11 0
-16 1 11 0
-16 -1 17 0
16 -17 0
1 -17 0
-3 -7 18 0
3 -18 0
7 -18 0
17 18 -15 0
-17 15 0
-18 15 0
c add_FA inputs=4, 8, cin=15, s=12, cout=19
-4 -8 -20 0
4 8 -20 0
4 -8 20 0
-4 8 20 0
-20 -15 -12 0
20 15 -12 0
20 -15 12 0
-20 15 12 0
-20 -15 21 0
20 -21 0
15 -21 0
-4 -8 22 0
4 -22 0
8 -22 0
21 22 -19 0
-21 19 0
-22 19 0
c add_FA inputs=5, 9, cin=19, s=13, cout=23
-5 -9 -24 0
5 9 -24 0
5 -9 24 0
-5 9 24 0
-24 -19 -13 0
24 19 -13 0
24 -19 13 0
-24 19 13 0
-24 -19 25 0
24 -25 0
19 -25 0
-5 -9 26 0
5 -26 0
9 -26 0
25 26 -23 0
-25 23 0
-26 23 0
c add_FA inputs=6, 10, cin=23, s=14, cout=27
-6 -10 -28 0
6 10 -28 0
6 -10 28 0
-6 10 28 0
-28 -23 -14 0
28 23 -14 0
28 -23 14 0
-28 23 14 0
-28 -23 29 0
28 -29 0
23 -29 0
-6 -10 30 0
6 -30 0
10 -30 0
29 30 -27 0
-29 27 0
-30 27 0
c generate_const(val=4, width=4). var_no=[31..34]
-31 0
-32 0
33 0
-34 0
c generate_EQ for two bitvectors, v1=[11...14], v2=[31...34]
c generate_BVXOR v1=[11...14] v2=[31...34]
-11 -31 -35 0
11 31 -35 0
11 -31 35 0
-11 31 35 0
-12 -32 -36 0
12 32 -36 0
12 -32 36 0
-12 32 36 0
-13 -33 -37 0
13 33 -37 0
13 -33 37 0
-13 33 37 0
-14 -34 -38 0
14 34 -38 0
14 -34 38 0
-14 34 38 0
c generate_OR_list(var=35, width=4) var out=39
35 36 37 38 -39 0
-35 39 0
-36 39 0
-37 39 0
-38 39 0
c generate_NOT id=internal!8 var=39, out id=internal!9 out var=40
-40 -39 0
40 39 0
c create_assert() id=internal!9 var=40
40 0



c always false
c always true
c add_FA inputs=3, 7, cin=1, s=11, cout=15
c add_FA inputs=4, 8, cin=15, s=12, cout=19
c add_FA inputs=5, 9, cin=19, s=13, cout=23
c add_FA inputs=6, 10, cin=23, s=14, cout=27
c generate_const(val=4, width=4). var_no=[31..34]
c generate_EQ for two bitvectors, v1=[11...14], v2=[31...34]
c generate_BVXOR v1=[11...14] v2=[31...34]
c generate_OR_list(var=35, width=4) var out=39
c generate_NOT id=internal!8 var=39, out id=internal!9 out var=40
c create_assert() id=internal!9 var=40



I make these functions add variable numbers to comments. And you can see how all the signals are routed inside each full-adder.

generate_EQ() function makes two bitvectors equal by XOR-ing two bitvectors. Resulting bitvector is then OR-ed, and result must be zero.

Again, this SAT instance is small enough to be handled by my simple SAT backtracking solver:

SAT
-1 2 -3 -4 -5 -6 -7 -8 9 -10 -11 -12 13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 24 -25 -26 -27 -28 -29 -30 -31 -32 33 -34 -35 -36
-37 -38 -39 40 0
SAT
-1 2 -3 -4 -5 6 -7 -8 9 10 -11 -12 13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 24 -25 -26 27 -28 -29 30 -31 -32 33 -34 -35 -36 -37
-38 -39 40 0

...

SAT
-1 2 3 4 5 -6 7 -8 9 10 -11 -12 13 -14 15 -16 -17 18 19 20 21 -22 23 -24 -25 26 27 28 29 -30 -31 -32 33 -34 -35 -36 -37 -38 -39 40 0
SAT
-1 2 3 4 5 6 7 -8 9 -10 -11 -12 13 -14 15 -16 -17 18 19 20 21 -22 23 -24 -25 26 27 28 29 -30 -31 -32 33 -34 -35 -36 -37 -38 -39 40 0
UNSAT
solutions= 16


Another post in my blog where I write about adders in SAT: https://yurichev.com/blog/factor_SAT/.