TY - GEN
T1 - Mixed radix weight totalizer encoding for pseudo-boolean constraints
AU - Zha, Aolong
AU - Uemura, Naoki
AU - Koshimura, Miyuki
AU - Fujita, Hiroshi
N1 - Funding Information:
This work was supported by JSPS KAKENHI Grant Numbers JP16K00304 and JP17K00307.
Publisher Copyright:
© 2017 IEEE.
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
T2 - 29th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2017
Y2 - 6 November 2017 through 8 November 2017
ER -