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.