A Hybrid Encoding of Pseudo-Boolean Constraints into CNF

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

Fingerprint

Computational complexity

All Science Journal Classification (ASJC) codes

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

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

A Hybrid Encoding of Pseudo-Boolean Constraints into CNF. / Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi.

Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017. Institute of Electrical and Electronics Engineers Inc., 2018. p. 9-12 (Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017).

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

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. Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017, Institute of Electrical and Electronics Engineers Inc., pp. 9-12, 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017, Taipei, Taiwan, Province of China, 12/1/17. https://doi.org/10.1109/TAAI.2017.15
Zha A, Koshimura M, Fujita H. A Hybrid Encoding of Pseudo-Boolean Constraints into CNF. In Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017. Institute of Electrical and Electronics Engineers Inc. 2018. p. 9-12. (Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017). https://doi.org/10.1109/TAAI.2017.15
Zha, Aolong ; Koshimura, Miyuki ; Fujita, Hiroshi. / A Hybrid Encoding of Pseudo-Boolean Constraints into CNF. Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017. Institute of Electrical and Electronics Engineers Inc., 2018. pp. 9-12 (Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017).
@inproceedings{175153f38653493a95e1c18b25bb53b4,
title = "A Hybrid Encoding of Pseudo-Boolean Constraints into CNF",
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.",
author = "Aolong Zha and Miyuki Koshimura and Hiroshi Fujita",
year = "2018",
month = "5",
day = "9",
doi = "10.1109/TAAI.2017.15",
language = "English",
series = "Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "9--12",
booktitle = "Proceedings - 2017 Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017",
address = "United States",

}

TY - GEN

T1 - A Hybrid Encoding of Pseudo-Boolean Constraints into CNF

AU - Zha, Aolong

AU - Koshimura, Miyuki

AU - Fujita, Hiroshi

PY - 2018/5/9

Y1 - 2018/5/9

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

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

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

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

U2 - 10.1109/TAAI.2017.15

DO - 10.1109/TAAI.2017.15

M3 - Conference contribution

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

SP - 9

EP - 12

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

PB - Institute of Electrical and Electronics Engineers Inc.

ER -