Re: [sage-support] Was: Graph plotting and labels
Christian Szegedy
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.
On 12/17/09, VictorMiller <victor...@gmail.com> 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 sage-s...@googlegroups.com
> To unsubscribe from this group, send email to sage-support...@googlegroups.com
> For more options, visit this group at http://groups.google.com/group/sage-support
> URL: http://www.sagemath.org
>
David Joyner
<christia...@gmail.com> 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.
>
FYI, there has been some efforts towards creating a minisat spkg:
http://trac.sagemath.org/sage_trac/ticket/418
http://trac.sagemath.org/sage_trac/ticket/5671
William Stein
<christia...@gmail.com> 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
--
William Stein
Associate Professor of Mathematics
University of Washington
http://wstein.org