Modulo based CNF encoding of cardinality constraints and its evaluation

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

Research output: Contribution to journalArticlepeer-review


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
Issue number2
Publication statusPublished - 2013

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering


Dive into the research topics of 'Modulo based CNF encoding of cardinality constraints and its evaluation'. Together they form a unique fingerprint.

Cite this