Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Citations (Scopus)

Abstract

Totalizer (TO) by Bailleux et al. and Half Sorting Network (HS) 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 in terms 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
Title of host publicationProceedings - 25th International Conference on Tools with Artificial Intelligence, ICTAI 2013
Pages9-17
Number of pages9
DOIs
Publication statusPublished - 2013
Event25th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2013 - Washington, DC, United States
Duration: Nov 4 2013Nov 6 2013

Publication series

NameProceedings - International Conference on Tools with Artificial Intelligence, ICTAI
ISSN (Print)1082-3409

Other

Other25th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2013
CountryUnited States
CityWashington, DC
Period11/4/1311/6/13

All Science Journal Classification (ASJC) codes

  • Software
  • Artificial Intelligence
  • Computer Science Applications

Fingerprint Dive into the research topics of 'Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers'. Together they form a unique fingerprint.

Cite this