Modulo based CNF encoding of cardinality constraints and its evaluation

Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita

Research output: Contribution to journalArticle

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.

Original languageEnglish
Pages (from-to)85-92
Number of pages8
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Volume18
Issue number2
Publication statusPublished - 2013

Fingerprint

Adders

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering

Cite this

Modulo based CNF encoding of cardinality constraints and its evaluation. / Ogawa, Toru; Liu, Yangyang; Hasegawa, Ryuzo; Koshimura, Miyuki; Fujita, Hiroshi.

In: Research Reports on Information Science and Electrical Engineering of Kyushu University, Vol. 18, No. 2, 2013, p. 85-92.

Research output: Contribution to journalArticle

@article{1fb9c5edbc8c4df6922abed1e735b8be,
title = "Modulo based CNF encoding of cardinality constraints and its evaluation",
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.",
author = "Toru Ogawa and Yangyang Liu and Ryuzo Hasegawa and Miyuki Koshimura and Hiroshi Fujita",
year = "2013",
language = "English",
volume = "18",
pages = "85--92",
journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",
issn = "1342-3819",
publisher = "Kyushu University, Faculty of Science",
number = "2",

}

TY - JOUR

T1 - Modulo based CNF encoding of cardinality constraints and its evaluation

AU - Ogawa, Toru

AU - Liu, Yangyang

AU - Hasegawa, Ryuzo

AU - Koshimura, Miyuki

AU - Fujita, Hiroshi

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84904537786&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84904537786&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:84904537786

VL - 18

SP - 85

EP - 92

JO - Research Reports on Information Science and Electrical Engineering of Kyushu University

JF - Research Reports on Information Science and Electrical Engineering of Kyushu University

SN - 1342-3819

IS - 2

ER -