Modulo Based CNF Encoding of Cardinality Constraints and Its Evaluation

DOI HANDLE Open Access
  • Ogawa Toru
    Department of Informatics, Graduate School of Information Science and Engineering, Kyushu University : Graduate Student
  • Liu Yangyang
    Department of Informatics, Graduate School of Information Science and Engineering, Kyushu University : Graduate Student
  • Hasegawa Ryuzo
    Department of Informatics, Faculty of Information Science and Electrical Engineering, Kyushu University
  • Koshimura Miyuki
    Department of Informatics, Faculty of Information Science and Electrical Engineering, Kyushu University
  • Fujita Hiroshi
    Department of Informatics, Faculty of Information Science and Electrical Engineering, Kyushu University

Bibliographic Information

Other Title
  • Modulo計算に基づく基数制約のCNF符号化方式の提案と評価

Search this article

Abstract

Totalizer (TO) proposed by Bailleux et al. and Half Sort (HS) proposed by Asin et al. are typical CNF encoding methods of cardinality constraint. The former is based on unary adder, while the latter is based on odd-even merge. Although TO is inferior to HS interms of the number of clauses, TO is superior to HS in terms of the number of variables. We propose a new method called Modulo Totalizer (MTO) to overcome the disadvantage of TO. As an application, we have developed a partial MaxSAT solver with MTO. Preliminary experimental results show that our MTO based MaxSAT solver is comparable to or surpass the conventional TO based maxsat solvers.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

  • CRID
    1390290699814852352
  • NII Article ID
    120005306729
  • NII Book ID
    AN10569524
  • DOI
    10.15017/26858
  • ISSN
    21880891
    13423819
  • HANDLE
    2324/26858
  • Text Lang
    ja
  • Data Source
    • JaLC
    • IRDB
    • CiNii Articles
    • KAKEN
  • Abstract License Flag
    Allowed

Report a problem

Back to top