The search functionality is under construction.
The search functionality is under construction.

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

Tomu MAKITA, Atsuki NAGAO, Tatsuki OKADA, Kazuhisa SETO, Junichi TERUYAMA

  • Full Text Views

    112

  • Cite this
  • Free PDF (1.8MB)

Summary :

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.

Publication
IEICE TRANSACTIONS on Fundamentals Vol.E105-A No.9 pp.1298-1308
Publication Date
2022/09/01
Publicized
2022/03/08
Online ISSN
1745-1337
DOI
10.1587/transfun.2021EAP1120
Type of Manuscript
PAPER
Category
Algorithms and Data Structures

Authors

Tomu MAKITA
  Seikei University
Atsuki NAGAO
  Ochanomizu University
Tatsuki OKADA
  Seikei University
Kazuhisa SETO
  Hokkaido University
Junichi TERUYAMA
  University of Hyogo

Keyword