A Satisfiability Algorithm for Deterministic Width-2 Branching Programs

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

doi:10.1587/transfun.2021EAP1120

IEICE TRANSACTIONS on Fundamentals

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

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

Full Text Views

58

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/2^{O(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

satisfiability, width-k branching program, greedy restriction, moderately exponential time, exact algorithm

Cite this

Copy

Tomu MAKITA, Atsuki NAGAO, Tatsuki OKADA, Kazuhisa SETO, Junichi TERUYAMA, "A Satisfiability Algorithm for Deterministic Width-2 Branching Programs" in IEICE TRANSACTIONS on Fundamentals, vol. E105-A, no. 9, pp. 1298-1308, September 2022, doi: 10.1587/transfun.2021EAP1120.
Abstract: 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/2^{O(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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.2021EAP1120/_p

Copy

@ARTICLE{e105-a_9_1298,
author={Tomu MAKITA, Atsuki NAGAO, Tatsuki OKADA, Kazuhisa SETO, Junichi TERUYAMA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={A Satisfiability Algorithm for Deterministic Width-2 Branching Programs},
year={2022},
volume={E105-A},
number={9},
pages={1298-1308},
abstract={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/2^{O(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.},
keywords={},
doi={10.1587/transfun.2021EAP1120},
ISSN={1745-1337},
month={September},}

Copy

TY - JOUR
TI - A Satisfiability Algorithm for Deterministic Width-2 Branching Programs
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1298
EP - 1308
AU - Tomu MAKITA
AU - Atsuki NAGAO
AU - Tatsuki OKADA
AU - Kazuhisa SETO
AU - Junichi TERUYAMA
PY - 2022
DO - 10.1587/transfun.2021EAP1120
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E105-A
IS - 9
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - September 2022
AB - 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/2^{O(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.
ER -

IEICE TRANSACTIONS on Fundamentals