N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT

Aolong Zha, Miyuki Koshimura, Hiroshi Fujita

研究成果: Contribution to journalArticle査読

2 被引用数 (Scopus)

抄録

Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

本文言語英語
ページ(範囲)133-161
ページ数29
ジャーナルConstraints
24
2
DOI
出版ステータス出版済み - 4 15 2019

All Science Journal Classification (ASJC) codes

  • Software
  • Discrete Mathematics and Combinatorics
  • Computational Theory and Mathematics
  • Artificial Intelligence

フィンガープリント 「N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル