Construction of an ROBDD for a PB-Constraint in Band Form and Related Techniques for PB-Solvers

• SAKAI Masahiko

  Graduate School of Information Science, Nagoya University

• NABESHIMA Hidetomo

  Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi

抄録

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.

収録刊行物

• IEICE Transactions on Information and Systems

  IEICE Transactions on Information and Systems E98.D (6), 1121-1127, 2015

  一般社団法人 電子情報通信学会

キーワード

• reduced ordered BDD
• Pesudo-Boolean constraint
• optimization problem

詳細情報

• CRID: 1390001204378476288
• NII論文ID: 130005072390
• DOI: 10.1587/transinf.2014fop0007
• ISSN: 17451361
• ISSN: 09168532
• Web Site: https://www.jstage.jst.go.jp/article/transinf/E98.D/6/E98.D_2014FOP0007/_pdf
• 本文言語コード: en
• データソース種別:
  • JaLC
  • Crossref
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可