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

Aolong Zha, Miyuki Koshimura, Hiroshi Fujita

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)133-161
Number of pages29
JournalConstraints
Volume24
Issue number2
DOIs
Publication statusPublished - Apr 15 2019

All Science Journal Classification (ASJC) codes

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

Fingerprint Dive into the research topics of 'N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT'. Together they form a unique fingerprint.

Cite this