Simple adder in SAT/SMT

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):

More info from wikipedia: https://en.wikipedia.org/wiki/Adder_(electronics).

I'm implementing full-adder like this:

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

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);
	add_clause2(-v1, var_out);
	add_clause2(-v2, var_out);
};

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

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_XOR(a, b, XOR1_out);
	add_Tseitin_XOR(XOR1_out, cin, s);
	add_Tseitin_AND(XOR1_out, cin, AND1_out);
	add_Tseitin_AND(a, b, AND2_out);
	add_Tseitin_OR2(AND1_out, AND2_out, cout);
};

( https://github.com/DennisYurichev/MK85/blob/master/MK85.c )

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.

Then I connect full-adders to create a n-bit adder:

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

	...

	*sum=create_internal_variable("adder_sum", TY_BITVEC, a->width);

	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++)
	{
		*carry_out=create_internal_variable("adder_carry", TY_BOOL, 1);
		add_FA(a->var_no+i, b->var_no+i, carry, (*sum)->var_no+i, (*carry_out)->var_no);
		// newly created carry_out is a carry_in for the next full-adder:
		carry=(*carry_out)->var_no;
	};
};

( https://github.com/DennisYurichev/MK85/blob/master/MK85.c )

Let's take a look on output CNF file:

p cnf 40 114
c always false
-1 0
c always true
2 0
c generate_adder
c add_FA inputs=3, 7, cin=1, s=11, cout=15
c add_Tseitin_XOR 16=3^7
-3 -7 -16 0
3 7 -16 0
3 -7 16 0
-3 7 16 0
c add_Tseitin_XOR 11=16^1
-16 -1 -11 0
16 1 -11 0
16 -1 11 0
-16 1 11 0
c add_Tseitin_AND 17=16&1
-16 -1 17 0
16 -17 0
1 -17 0
c add_Tseitin_AND 18=3&7
-3 -7 18 0
3 -18 0
7 -18 0
c add_Tseitin_OR2 15=17|18
17 18 -15 0
-17 15 0
-18 15 0
c add_FA inputs=4, 8, cin=15, s=12, cout=19
c add_Tseitin_XOR 20=4^8
-4 -8 -20 0
4 8 -20 0
4 -8 20 0
-4 8 20 0
c add_Tseitin_XOR 12=20^15
-20 -15 -12 0
20 15 -12 0
20 -15 12 0
-20 15 12 0
c add_Tseitin_AND 21=20&15
-20 -15 21 0
20 -21 0
15 -21 0
c add_Tseitin_AND 22=4&8
-4 -8 22 0
4 -22 0
8 -22 0
c add_Tseitin_OR2 19=21|22
21 22 -19 0
-21 19 0
-22 19 0
c add_FA inputs=5, 9, cin=19, s=13, cout=23
c add_Tseitin_XOR 24=5^9
-5 -9 -24 0
5 9 -24 0
5 -9 24 0
-5 9 24 0
c add_Tseitin_XOR 13=24^19
-24 -19 -13 0
24 19 -13 0
24 -19 13 0
-24 19 13 0
c add_Tseitin_AND 25=24&19
-24 -19 25 0
24 -25 0
19 -25 0
c add_Tseitin_AND 26=5&9
-5 -9 26 0
5 -26 0
9 -26 0
c add_Tseitin_OR2 23=25|26
25 26 -23 0
-25 23 0
-26 23 0
c add_FA inputs=6, 10, cin=23, s=14, cout=27
c add_Tseitin_XOR 28=6^10
-6 -10 -28 0
6 10 -28 0
6 -10 28 0
-6 10 28 0
c add_Tseitin_XOR 14=28^23
-28 -23 -14 0
28 23 -14 0
28 -23 14 0
-28 23 14 0
c add_Tseitin_AND 29=28&23
-28 -23 29 0
28 -29 0
23 -29 0
c add_Tseitin_AND 30=6&10
-6 -10 30 0
6 -30 0
10 -30 0
c add_Tseitin_OR2 27=29|30
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]
c add_Tseitin_XOR 35=11^31
-11 -31 -35 0
11 31 -35 0
11 -31 35 0
-11 31 35 0
c add_Tseitin_XOR 36=12^32
-12 -32 -36 0
12 32 -36 0
12 -32 36 0
-12 32 36 0
c add_Tseitin_XOR 37=13^33
-13 -33 -37 0
13 33 -37 0
13 -33 37 0
-13 33 37 0
c add_Tseitin_XOR 38=14^34
-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
c add_Tseitin_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

Filter out comments:

c always false
c always true
c generate_adder
c add_FA inputs=3, 7, cin=1, s=11, cout=15
c add_Tseitin_XOR 16=3^7
c add_Tseitin_XOR 11=16^1
c add_Tseitin_AND 17=16&1
c add_Tseitin_AND 18=3&7
c add_Tseitin_OR2 15=17|18
c add_FA inputs=4, 8, cin=15, s=12, cout=19
c add_Tseitin_XOR 20=4^8
c add_Tseitin_XOR 12=20^15
c add_Tseitin_AND 21=20&15
c add_Tseitin_AND 22=4&8
c add_Tseitin_OR2 19=21|22
c add_FA inputs=5, 9, cin=19, s=13, cout=23
c add_Tseitin_XOR 24=5^9
c add_Tseitin_XOR 13=24^19
c add_Tseitin_AND 25=24&19
c add_Tseitin_AND 26=5&9
c add_Tseitin_OR2 23=25|26
c add_FA inputs=6, 10, cin=23, s=14, cout=27
c add_Tseitin_XOR 28=6^10
c add_Tseitin_XOR 14=28^23
c add_Tseitin_AND 29=28&23
c add_Tseitin_AND 30=6&10
c add_Tseitin_OR2 27=29|30
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 add_Tseitin_XOR 35=11^31
c add_Tseitin_XOR 36=12^32
c add_Tseitin_XOR 37=13^33
c add_Tseitin_XOR 38=14^34
c generate_OR_list(var=35, width=4) var out=39
c add_Tseitin_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/.

→ [back to the main page]