Full Text Views
112
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.
Tomu MAKITA
Seikei University
Atsuki NAGAO
Ochanomizu University
Tatsuki OKADA
Seikei University
Kazuhisa SETO
Hokkaido University
Junichi TERUYAMA
University of Hyogo
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
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/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.
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/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.},
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/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.
ER -