Skip to main content

Questions tagged [bdd]

Questions related to binary decision diagrams.

Filter by
Sorted by
Tagged with
0 votes
0 answers
14 views

ROBDDs heuristics for optimal variable ordering

I have this slide about how a BDD can vary in size depending on the order of the boolean variables fixed for it, and how it is NP-Complete to find the optimal ordering. It says there are heuristics ...
revision's user avatar
0 votes
1 answer
59 views

What's the relation between DPLL and BDDs?

BDDs are a way of representing Boolean formulas. DPLL is an algorithm to determine satisfiability of Boolean formulas. My understanding is that the two are used for SAT solving. How are they combined?
user1868607's user avatar
  • 2,194
2 votes
0 answers
162 views

Efficient integer multiplication using BDDs and fixed point

Suppose we have two sets A,B of size n,k respectively, being sets of nonnegative integers each encoded with N bits, and we'd like to form a set of bitstrings of length 3N and [maximum] size n*k such ...
Troy McClure's user avatar
0 votes
2 answers
248 views

Compact Shared Reduced Binary Decision Diagrams with negated identifiers

Consider a BDD implementation in which each bdd in the system has a unique positive integer identifying it (thanks to canonicity and as common implementation designs follow, by utilizing a hashmap). I ...
Troy McClure's user avatar
0 votes
2 answers
527 views

BDD to CNF in linear time

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 ...
nrofis's user avatar
  • 198
1 vote
0 answers
66 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
Lance's user avatar
  • 2,265
1 vote
0 answers
78 views

Understanding a Single Step in the Model Checking Algorithm

This answer explains roughly how to convert a nested boolean function into a Binary Decision Diagram (BDD). This question is about how to structure the states for the BDD. Now in this question I am ...
Lance's user avatar
  • 2,265
3 votes
1 answer
1k views

What is the main difference between binary decision tree and binary decision diagram(BDD)?

What is the main difference between binary decision tree and binary decision diagram(BDD)? From what I can tell I only understand that a binary decision diagram is a more compact representation ...
Teodorico Levoff's user avatar
2 votes
1 answer
481 views

Multiplication function BDD size lower bounds

Randal Bryant developed an exponential size lower bound for any BDD encoding the middle bit output of the multiplication function, regardless of variable permutation. But at the same time the ...
user avatar
0 votes
1 answer
121 views

Creating a decision tree?

So I'm trying to split on an attribute "Color" that has possible values (Blue,Green,Red,Orange,Pink). I'm splitting on entropy values, and the best split can either be Multi-Way 5, Multi-Way 4, ...
ocean800's user avatar
  • 125
3 votes
1 answer
104 views

The complexity of BDD Synchronous Composition

As shown in Byrant's original paper, the time complexity of (single-variable) composition algorithm is cubic, and it is a tight upper bound. My question is about synchronous composition, written as $$...
doganulus's user avatar
  • 346
3 votes
0 answers
56 views

Knowing if I have an optimal ordering for a OBDD

I'm learning about OBDD and I have learned that the size of a reduced OBDD (ROBDD) is dependent on the ordering of the variables, and that finding an optimal ordering is an NP hard problem. Say I ...
Belgi's user avatar
  • 267
2 votes
1 answer
523 views

What are the differences between parse and decision trees?

I have created a parse tree for the formula: a∧¬(b∨c)∨¬d∧(¬b) successfully. I am now asked to create a decision tree for the same formula. What are the main differences between a parse tree and a ...
Djoni's user avatar
  • 33
3 votes
1 answer
214 views

Counting words that satisfy SAT-like constraints with BDDs

I have the following #P-complete problem: Given an alphabet $\Sigma$ and a matrix $M$ where each entry can be a symbol from $\Sigma$ or the wildcard symbol $*$, find the number of strings $s$ with ...
Elliot Gorokhovsky's user avatar
0 votes
1 answer
121 views

Is the number of nodes in an ORBDD 2n + 2?

Wikipedia says that the number of nodes in a ORBDD (Order Reduced Binary Decision Diagrams) of order $x_1 < x_2 < \dots < x_{2n}$ is $2n + 2$. But I can't find proof. Anyone?
kaitlynrutledge's user avatar
2 votes
0 answers
312 views

Difference between fully-reduced BDD and quasi-reduced BDD

I am trying to figure out difference between fully- and quasi-reduced BDDs. I have read a lot of material but still it is not very clear. As I am trying to figure out the quasi reduced version for ...
compengr's user avatar