0
$\begingroup$

I have a book from my university that claims:

There is an linear algorithm that can convert BDD to CNF in linear time, and generate CNF in linear length of the BDD size (number of nodes).

Then they wrote an exercise to find one...

Actually I tried to do so, I thought to find the paths that brings me to 0, and then translate them to clause (with the opposite value of the variables), and use Tseytin transformation to create linear length of CNF.

The problem are:

  1. How can I find all the paths to 0? I thought about DFS but it seems to be complex task for DFS because I need the variables value (the naive algorithm is exponential)
  2. The other problem is the variables to add, when should I create a new variable, every move? It can cause an exponential number of variables, which is not good.

So what is the correct algorithm to do that?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
0
$\begingroup$

This is a nice exercise. I'll give you a series of hints. Click on each hint only after you've spent a good amount of time thinking on the previous one. You'll get the most value by solving this on your own.

Hint #1:

Add extra variables.

Hint #2:

Use the Tseitin transform. Review to convert CircuitSAT to SAT.

Hint #3:

Introduce a boolean variable $x_v$ for each node $v$ in the BDD.

Hint #4:

The idea is that $x_v$ should be true iff the path you follow goes through $x_v$. Can you write clauses to ensure all of this?

Improve this answer
$\endgroup$
3
  • $\begingroup$ Actually I thought that is the direction of the solution. But first of all, how do you check every path in the BDD in linear time? $\endgroup$
    – nrofis
    Jun 9, 2018 at 9:21
  • $\begingroup$ @nrofis, you don't. You do something for each node in the BDD, not something for each path in the BDD. In the reduction from CircuitSAT to SAT, how do you check every path through the circuit? You don't. $\endgroup$
    – D.W. ♦
    Jun 9, 2018 at 15:05
  • $\begingroup$ Can you please check my solution? $\endgroup$
    – nrofis
    Jun 13, 2018 at 8:58
0
$\begingroup$

Thanks to D.W. hints here is the solution:

Let's introduce a boolean variable $x_v$ for each node $v$ in the BDD.

Start scanning the BDD from the leaf $1$ backward (with BFS for example). For each node that we visit, we will use Tseitin transform and we will be treated as an Or Gate. Its parents (in the original BDD direction) will be the input (the value of the variable of the parent should be the same as the edge in the BDD) and it will be the output. At the end of the search, we will combine each such CNF with conjunctions and will get one CNF that represents the BDD.

The search is done in linear time. Let $n$ to be the number of the vertex in the BDD. Each node adds at most 3 clauses (for the Or gate) and each clause has $n$ variables at most. So the complexity of the CNF length is $O(n*3n)=O(n^2)$ which means that we have linear running time and linear CNF length.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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