A Hybrid Encoding of Pseudo-Boolean Constraints into CNF

Aolong Zha, Miyuki Koshimura, Hiroshi Fujita

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

1 Citation (Scopus)

Abstract

Many NP-hard problems are commonly expressed with pseudo-Boolean (PB) constraints, which is a linear arithmetic constraint over Boolean variables. Conjunctive Normal Form (CNF) encoding always plays an important role in solving these constraints. In this paper, we propose Weighted Modulo Totalizer (WMTO) which is a hybrid CNF encoding of PB constraints between Modulo Totalizer (MTO) and Weighted Totalizer (WTO). WMTO uses less clauses and auxiliary variables than each of them. Our experimental results show that WMTO encodes the constraints compactly and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

Original languageEnglish
Title of host publicationProceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages9-12
Number of pages4
ISBN (Electronic)9781538642030
DOIs
Publication statusPublished - May 9 2018
Event2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017 - Taipei, Taiwan, Province of China
Duration: Dec 1 2017Dec 3 2017

Publication series

NameProceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017

Other

Other2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017
CountryTaiwan, Province of China
CityTaipei
Period12/1/1712/3/17

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computer Networks and Communications
  • Computer Science Applications
  • Human-Computer Interaction

Fingerprint Dive into the research topics of 'A Hybrid Encoding of Pseudo-Boolean Constraints into CNF'. Together they form a unique fingerprint.

  • Cite this

    Zha, A., Koshimura, M., & Fujita, H. (2018). A Hybrid Encoding of Pseudo-Boolean Constraints into CNF. In Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017 (pp. 9-12). (Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/TAAI.2017.15