Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A moderately exponential time algorithm for k-IBDD satisfiability
Nagao A., Seto K., Teruyama J. Algorithmica80 (10):2725-2741,2018.Type:Article
Date Reviewed: Aug 15 2018

Branching programs can be modeled using binary decision diagrams (BDDs), which are rooted directed acyclic graphs with vertices labeled using variables of the program, and two sink nodes representing zero and one. In an ordered BDD (OBDD), the order of the variables is the same in “all paths from the root to any sink.” An extension of this structure is a k-OBDD, which contains k layers of OBDDs.

Given a branching program, its satisfiability problem is “to determine whether there [is] an assignment ... to the input variables such that the path corresponding to [that assignment] can reach the 1-sink.” Here, the authors consider the satisfiability of k-indexed BDD (k-IBDD), which extends k-OBDD such that the variables in each of the k layers may have different orders.

The authors’ technique consists of extending earlier known methods of conjunction for deterministic OBDDs to nondeterministic OBDDs. The authors show that, given a nondeterministic OBDD, construction of a nondeterministic OBDD with the variable orders reversed can be done in time linear to the size of the original OBDD.

The authors explain:

Given a k-IBDD, the proposed algorithm calculates the longest common monotone sequence of [the k] variable orders. We then assign 0 or 1 to the variables except for those in the sequences.

This results in a k-IBDD where variables in each layer are either in a given order or its reverse. Because reversing variable order is efficient, such a k-IBDD can be transformed to a k-OBDD. By modifying earlier known methods, the k-OBDD is transformed into an OBDD for which satisfiability is solved in polynomial time.

The authors start with a good introduction that sufficiently covers the preliminaries in detail. They then proceed through a series of theoretical results that prove the complexity, before presenting their algorithm. Overall, an impressive work that will be of immense interest to students and researchers in the field.

Reviewer:  Paparao Kavalipati Review #: CR146202 (1811-0586)
Bookmark and Share
  Featured Reviewer  
 
Algorithm Design And Analysis (G.4 ... )
 
 
Decision Problems (F.4.2 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Algorithm Design And Analysis": Date
Numerical recipes
Sprott J., Cambridge University Press, New York, NY, 1991. Type: Book (9780521406895)
Dec 1 1992
An interactive calculus theorem-prover for continuity properties
Suppes P., Takahashi S. Journal of Symbolic Computation 7(6): 573-590, 1989. Type: Article
Aug 1 1990
The numerical methods programming projects book
Grandine T., Oxford University Press, Inc., New York, NY, 1990. Type: Book (9789780198533870)
Mar 1 1991
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy