Mixed radix weight totalizer encoding for pseudo-boolean constraints

Aolong Zha, Naoki Uemura, Miyuki Koshimura, Hiroshi Fujita

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

1 Citation (Scopus)

Abstract

Many problems in various fields can be expressed as the problem of optimizing the value of a pseudo-Boolean constraint which is a linear constraint over Boolean variables. This paper proposes a new technique, called Mixed Radix Weight Totalizer Encoding (MRWTE), which encodes pseudo-Boolean constraints into clauses that can be handled by a standard SAT solver. This new technique will allow us to fully exploit the latest improvements in SAT research. Unlike other encodings, the number of auxiliary variables required for MRWTE does not depend on the magnitudes of the coefficients. Instead, it depends on the number of distinct combinations of the coefficients. Our experimental results show that MRWTE compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-The-Art SAT solver.

Original languageEnglish
Title of host publicationProceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017
PublisherIEEE Computer Society
Pages868-875
Number of pages8
ISBN (Electronic)9781538638767
DOIs
Publication statusPublished - Jun 4 2018
Event29th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2017 - Boston, United States
Duration: Nov 6 2017Nov 8 2017

Publication series

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

Other

Other29th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2017
CountryUnited States
CityBoston
Period11/6/1711/8/17

All Science Journal Classification (ASJC) codes

  • Software
  • Artificial Intelligence
  • Computer Science Applications

Cite this

Zha, A., Uemura, N., Koshimura, M., & Fujita, H. (2018). Mixed radix weight totalizer encoding for pseudo-boolean constraints. In Proceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017 (pp. 868-875). (Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI; Vol. 2017-November). IEEE Computer Society. https://doi.org/10.1109/ICTAI.2017.00135

Mixed radix weight totalizer encoding for pseudo-boolean constraints. / Zha, Aolong; Uemura, Naoki; Koshimura, Miyuki; Fujita, Hiroshi.

Proceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017. IEEE Computer Society, 2018. p. 868-875 (Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI; Vol. 2017-November).

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

Zha, A, Uemura, N, Koshimura, M & Fujita, H 2018, Mixed radix weight totalizer encoding for pseudo-boolean constraints. in Proceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017. Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI, vol. 2017-November, IEEE Computer Society, pp. 868-875, 29th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2017, Boston, United States, 11/6/17. https://doi.org/10.1109/ICTAI.2017.00135
Zha A, Uemura N, Koshimura M, Fujita H. Mixed radix weight totalizer encoding for pseudo-boolean constraints. In Proceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017. IEEE Computer Society. 2018. p. 868-875. (Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI). https://doi.org/10.1109/ICTAI.2017.00135
Zha, Aolong ; Uemura, Naoki ; Koshimura, Miyuki ; Fujita, Hiroshi. / Mixed radix weight totalizer encoding for pseudo-boolean constraints. Proceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017. IEEE Computer Society, 2018. pp. 868-875 (Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI).
@inproceedings{f9a55cbf981d4072ba693720395d0e9a,
title = "Mixed radix weight totalizer encoding for pseudo-boolean constraints",
abstract = "Many problems in various fields can be expressed as the problem of optimizing the value of a pseudo-Boolean constraint which is a linear constraint over Boolean variables. This paper proposes a new technique, called Mixed Radix Weight Totalizer Encoding (MRWTE), which encodes pseudo-Boolean constraints into clauses that can be handled by a standard SAT solver. This new technique will allow us to fully exploit the latest improvements in SAT research. Unlike other encodings, the number of auxiliary variables required for MRWTE does not depend on the magnitudes of the coefficients. Instead, it depends on the number of distinct combinations of the coefficients. Our experimental results show that MRWTE compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-The-Art SAT solver.",
author = "Aolong Zha and Naoki Uemura and Miyuki Koshimura and Hiroshi Fujita",
year = "2018",
month = "6",
day = "4",
doi = "10.1109/ICTAI.2017.00135",
language = "English",
series = "Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI",
publisher = "IEEE Computer Society",
pages = "868--875",
booktitle = "Proceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017",
address = "United States",

}

TY - GEN

T1 - Mixed radix weight totalizer encoding for pseudo-boolean constraints

AU - Zha, Aolong

AU - Uemura, Naoki

AU - Koshimura, Miyuki

AU - Fujita, Hiroshi

PY - 2018/6/4

Y1 - 2018/6/4

N2 - Many problems in various fields can be expressed as the problem of optimizing the value of a pseudo-Boolean constraint which is a linear constraint over Boolean variables. This paper proposes a new technique, called Mixed Radix Weight Totalizer Encoding (MRWTE), which encodes pseudo-Boolean constraints into clauses that can be handled by a standard SAT solver. This new technique will allow us to fully exploit the latest improvements in SAT research. Unlike other encodings, the number of auxiliary variables required for MRWTE does not depend on the magnitudes of the coefficients. Instead, it depends on the number of distinct combinations of the coefficients. Our experimental results show that MRWTE compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-The-Art SAT solver.

AB - Many problems in various fields can be expressed as the problem of optimizing the value of a pseudo-Boolean constraint which is a linear constraint over Boolean variables. This paper proposes a new technique, called Mixed Radix Weight Totalizer Encoding (MRWTE), which encodes pseudo-Boolean constraints into clauses that can be handled by a standard SAT solver. This new technique will allow us to fully exploit the latest improvements in SAT research. Unlike other encodings, the number of auxiliary variables required for MRWTE does not depend on the magnitudes of the coefficients. Instead, it depends on the number of distinct combinations of the coefficients. Our experimental results show that MRWTE compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-The-Art SAT solver.

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

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

U2 - 10.1109/ICTAI.2017.00135

DO - 10.1109/ICTAI.2017.00135

M3 - Conference contribution

AN - SCOPUS:85048470441

T3 - Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI

SP - 868

EP - 875

BT - Proceedings - 2017 International Conference on Tools with Artificial Intelligence, ICTAI 2017

PB - IEEE Computer Society

ER -