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 \}$.


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.

  • 1
    $\begingroup$ 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 ϕ $\endgroup$
    – harold
    Oct 4, 2017 at 12:48
  • $\begingroup$ Sure, if it is not zero. $\endgroup$
    – racc44
    Oct 4, 2017 at 15:14
  • $\begingroup$ 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? $\endgroup$
    – D.W.
    Oct 4, 2017 at 21:00
  • $\begingroup$ 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"? $\endgroup$
    – D.W.
    Oct 4, 2017 at 21:08

1 Answer 1


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).$$

  • $\begingroup$ 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$? $\endgroup$
    – racc44
    Oct 5, 2017 at 11:25
  • 1
    $\begingroup$ @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}$. $\endgroup$
    – D.W.
    Oct 5, 2017 at 17:50
  • $\begingroup$ Nice! Do you know another paper or source which describes bit blasting? $\endgroup$
    – racc44
    Oct 5, 2017 at 20:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.