TY - GEN
T1 - Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers
AU - Ogawa, Toru
AU - Liu, Yangyang
AU - Hasegawa, Ryuzo
AU - Koshimura, Miyuki
AU - Fujita, Hiroshi
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84897740348&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84897740348&partnerID=8YFLogxK
U2 - 10.1109/ICTAI.2013.13
DO - 10.1109/ICTAI.2013.13
M3 - Conference contribution
AN - SCOPUS:84897740348
SN - 9781479929719
T3 - Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI
SP - 9
EP - 17
BT - Proceedings - 25th International Conference on Tools with Artificial Intelligence, ICTAI 2013
T2 - 25th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2013
Y2 - 4 November 2013 through 6 November 2013
ER -