# Bit Blasting Algorithm

I found a pseudo algorithm which describes bit blasting: click (page 156,157). I am trying to implement it in C, but I don't understand it yet completely. Let's make an example:

Assume our bit-vectors have only a length of 2 bits (for simplicity) and they are unsigned and out bit-vector formula looks as follows: $\phi = x \,\,\,\wedge\,\,\, y\mid 2 = z \,\,\,\wedge\,\,\, 1 < 3$.

Let's describe Boolean variables with $b_0, b_1,...$ ($x,y$ and $z$ are bit vectors).

The set of atoms would be $At(\phi) = \{ x,\,\,\, y\mid2=z,\,\,\, 1<3 \}$ and therefore the initially $\beta = e(\phi) = b_0 \,\,\,\wedge\,\,\, b_1 \,\,\,\wedge\,\,\, b_2$.

The set of terms would be $T(\phi) = \{ x,\,\,\, y, \,\,\, 2,\,\,\, z,\,\,\ 1,\,\,\,3 \}$.

# Algorithm

Line 2: $\beta$ is already set.

Line 3-5: We set the $t \in T(\phi)$ to Boolean variables, hence $x \rightarrow b_3, b_4\,$ - (because we said our bit-vectors only have a length of 2 bits), the same with $y$ and $z$, but what happens with constants? I would guess: $2 \rightarrow 1,0$ or more precise $2 \rightarrow b_7=1, \, b_8=0$.

So after line 5, our $T(\phi) = \{ b_3, b_4,..., b_{14}\}$.

Then I stuck, how does it go on? And how would the equisatisfiable Boolean formula $\beta$ look like after the algorithm? Other references to other algorithms would be also nice.

• x is not a boolean, so it doesn't make much sense to have a constraint "x is true" as you seem to have in your ϕ – harold Oct 4 '17 at 12:48
• Sure, if it is not zero. – racc44 Oct 4 '17 at 15:14
• Can you edit to provide a full citation for the paper/book you are referencing, so the question is still understandable if the link stops working, and so that others with a similar question about it will find this question via search? – D.W. Oct 4 '17 at 21:00
• Can you make the question sef-contained? Can you provide a self-contained definition of your notation -- what is $\beta$? Do I need to know? What are the "lines"? – D.W. Oct 4 '17 at 21:08

I assume the formula is

$$(x \ne 0) \land (y|2 = z) \land (1<3).$$

We can handle each clause of the conjunction separately. If $x=(b_3,b_4)$, then $x \ne 0$ translates to

$$b_3 \lor b_4.$$

If $y=(b_5,b_6)$ and $z=(b_7,b_8)$, then $y|2$ translates to $(b_5|1,b_6)$, which simplifies to $(1,b_6)$ (if you are doing simplification). Now $(1,b_6) = (b_7,b_8)$ translates to

$$(b_7=1) \land (b_6 = b_8),$$

which in CNF form is

$$b_7 \land (b_6 \lor \neg b_8) \land (\neg b_6 \lor b_8).$$

Finally, $1<3$ translates to True, if you are doing simplification. So, the final result is the conjunction of those:

$$(b_3 \lor b_4) \land (b_7) \land (b_6 \lor \neg b_8) \land (\neg b_6 \lor b_8).$$

• That makes it a lot clearer for me, thanks a lot. However, I don't actually understand what the given algorithm does from line 6-9, particularly line 8-9. And why we need $b_0 \,\,\wedge\,\, b_1 \,\,\wedge\,\, b_2$ as initialization (they call it the propositional skeleton of $\phi$). I will soon edit my question to make it self-containing. Can you also come up with a suggestion for something like $x + y = z$? – racc44 Oct 5 '17 at 11:25
• @racc44, one standard approach would be to build a bitvector representation for each subexpression. So if $x=(b_3,b_4)$ and $y=(b_5,b_6)$ and $z=(b_7,b_8)$ and we use $(b_9,b_{10})$ to represent $x+y$, you first write CNF for $b_3,b_4,b_5,b_6,b_9,b_{10}$ that represents addition (this can be done using the Tseitin transform on an adder circuit), then add CNF to enforce $b_7=b_9$ and $b_8=b_{10}$. – D.W. Oct 5 '17 at 17:50
• Nice! Do you know another paper or source which describes bit blasting? – racc44 Oct 5 '17 at 20:43