The search functionality is under construction.

Author Search Result

[Author] Tomu MAKITA(1hit)

1-1hit
  • A Satisfiability Algorithm for Deterministic Width-2 Branching Programs Open Access

    Tomu MAKITA  Atsuki NAGAO  Tatsuki OKADA  Kazuhisa SETO  Junichi TERUYAMA  

     
    PAPER-Algorithms and Data Structures

      Pubricized:
    2022/03/08
      Vol:
    E105-A No:9
      Page(s):
    1298-1308

    A branching program is a well-studied model of computation and a representation for Boolean functions. It is a directed acyclic graph with a unique root node, some accepting nodes, and some rejecting nodes. Except for the accepting and rejecting nodes, each node has a label with a variable and each outgoing edge of the node has a label with a 0/1 assignment of the variable. The satisfiability problem for branching programs is, given a branching program with n variables and m nodes, to determine if there exists some assignment that activates a consistent path from the root to an accepting node. The width of a branching program is the maximum number of nodes at any level. The satisfiability problem for width-2 branching programs is known to be NP-complete. In this paper, we present a satisfiability algorithm for width-2 branching programs with n variables and cn nodes, and show that its running time is poly(n)·2(1-µ(c))n, where µ(c)=1/2O(c log c). Our algorithm consists of two phases. First, we transform a given width-2 branching program to a set of some structured formulas that consist of AND and Exclusive-OR gates. Then, we check the satisfiability of these formulas by a greedy restriction method depending on the frequency of the occurrence of variables.