IEICE TRANSACTIONS on Information
Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers
Summary :
Pseudo-Boolean (PB) problems are Integer Linear Problem restricted to 0-1 variables. This paper discusses on acceleration techniques of PB-solvers that employ SAT-solving of combined CNFs each of which is produced from each PB-constraint via a binary decision diagram (BDD). Specifically, we show (i) an efficient construction of a reduced ordered BDD (ROBDD) from a constraint in band form l ≤ <Linear term> ≤ h, (ii) a CNF coding that produces two clauses for some nodes in an ROBDD obtained by (i), and (iii) an incremental SAT-solving of the binary/alternative search for minimizing values of a given goal function. We implemented the proposed constructions and report on experimental results.
- Publication
- IEICE TRANSACTIONS on Information Vol.E98-D No.6 pp.1121-1127
- Publication Date
- 2015/06/01
- Publicized
- 2015/02/13
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2014FOP0007
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approach)
- Category
- Foundation
Authors
Masahiko SAKAI
Nagoya University
Hidetomo NABESHIMA
University of Yamanashi
Keyword
Latest Issue
Copyrights notice of machine-translated contents
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.
Cite this
Copy
Masahiko SAKAI, Hidetomo NABESHIMA, "Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers" in IEICE TRANSACTIONS on Information,
vol. E98-D, no. 6, pp. 1121-1127, June 2015, doi: 10.1587/transinf.2014FOP0007.
Abstract: Pseudo-Boolean (PB) problems are Integer Linear Problem restricted to 0-1 variables. This paper discusses on acceleration techniques of PB-solvers that employ SAT-solving of combined CNFs each of which is produced from each PB-constraint via a binary decision diagram (BDD). Specifically, we show (i) an efficient construction of a reduced ordered BDD (ROBDD) from a constraint in band form l ≤ <Linear term> ≤ h, (ii) a CNF coding that produces two clauses for some nodes in an ROBDD obtained by (i), and (iii) an incremental SAT-solving of the binary/alternative search for minimizing values of a given goal function. We implemented the proposed constructions and report on experimental results.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2014FOP0007/_p
Copy
@ARTICLE{e98-d_6_1121,
author={Masahiko SAKAI, Hidetomo NABESHIMA, },
journal={IEICE TRANSACTIONS on Information},
title={Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers},
year={2015},
volume={E98-D},
number={6},
pages={1121-1127},
abstract={Pseudo-Boolean (PB) problems are Integer Linear Problem restricted to 0-1 variables. This paper discusses on acceleration techniques of PB-solvers that employ SAT-solving of combined CNFs each of which is produced from each PB-constraint via a binary decision diagram (BDD). Specifically, we show (i) an efficient construction of a reduced ordered BDD (ROBDD) from a constraint in band form l ≤ <Linear term> ≤ h, (ii) a CNF coding that produces two clauses for some nodes in an ROBDD obtained by (i), and (iii) an incremental SAT-solving of the binary/alternative search for minimizing values of a given goal function. We implemented the proposed constructions and report on experimental results.},
keywords={},
doi={10.1587/transinf.2014FOP0007},
ISSN={1745-1361},
month={June},}
Copy
TY - JOUR
TI - Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers
T2 - IEICE TRANSACTIONS on Information
SP - 1121
EP - 1127
AU - Masahiko SAKAI
AU - Hidetomo NABESHIMA
PY - 2015
DO - 10.1587/transinf.2014FOP0007
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E98-D
IS - 6
JA - IEICE TRANSACTIONS on Information
Y1 - June 2015
AB - Pseudo-Boolean (PB) problems are Integer Linear Problem restricted to 0-1 variables. This paper discusses on acceleration techniques of PB-solvers that employ SAT-solving of combined CNFs each of which is produced from each PB-constraint via a binary decision diagram (BDD). Specifically, we show (i) an efficient construction of a reduced ordered BDD (ROBDD) from a constraint in band form l ≤ <Linear term> ≤ h, (ii) a CNF coding that produces two clauses for some nodes in an ROBDD obtained by (i), and (iii) an incremental SAT-solving of the binary/alternative search for minimizing values of a given goal function. We implemented the proposed constructions and report on experimental results.
ER -
English
