On Thu, Dec 17, 2009 at 11:55 AM, Christian Szegedy <[email protected]> wrote: > Not an answer, but a side question (probably belongs to sage-devel, anyhow...) > > Why would you use BDDs in the first place? > For almost any applications, SAT-solvers beat BDDs by large margins, > and also have incremental implementations. One of the best (also > insustrially used) > SAT solvers: MiniSAT is available under the permissive MIT license.
There are probably some good reasons, given that Victor (the guy that is wrapping CUDD) is an expert in applications of SAT solvers, including MiniSAT. -- William > > > On 12/17/09, VictorMiller <[email protected]> wrote: >> I'm in the middle of implementing SAGE classes for binary decision >> diagrams using the library called CUDD (which is included in >> Polybori). Each BDD is actually a labeled DiGraph. It's standard in >> the BDD literature to draw pictures of the digraph as follows: >> >> the vertex label of a non-leaf is a decision node, and it's standard >> to label it with the variable name. Note that the same variable may >> appear in more than one node, so this is not the same as the vertex >> labeling convention for DiGraph in sage. Each decision node also >> always has two outgoing directed edges -- the true edge which is drawn >> with a solid line, and the false edge with a dotted line. Is there a >> way in the plotting package from graph to have different edge >> rendering depending on some criterion? It would also be nice if the >> graph package could be supplemented to allow extra labels to be >> associated with each vertex (besides its unique label), and to have an >> option for plot of just printing the extra information. It's also >> traditional in the BDD literature to print the leaves (terminal nodes) >> with boxes around them instead of circles. >> >> What do people think about some way of enriching the graph package to >> allow such things? >> >> Victor >> >> >> -- >> To post to this group, send email to [email protected] >> To unsubscribe from this group, send email to >> [email protected] >> For more options, visit this group at >> http://groups.google.com/group/sage-support >> URL: http://www.sagemath.org >> > > -- > To post to this group, send email to [email protected] > To unsubscribe from this group, send email to > [email protected] > For more options, visit this group at > http://groups.google.com/group/sage-support > URL: http://www.sagemath.org > -- William Stein Associate Professor of Mathematics University of Washington http://wstein.org -- To post to this group, send email to [email protected] To unsubscribe from this group, send email to [email protected] For more options, visit this group at http://groups.google.com/group/sage-support URL: http://www.sagemath.org
