N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT
N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT
复制标题
MaxSAT 伪布尔约束的 N 级基于模的 CNF 编码
DOI：
10.1007/s10601-018-9299-0
复制
发表时间：
2019
期刊：
影响因子：
1.6
通讯作者：
Hiroshi Fujita
中科院分区：
文献类型：
--
作者：
Aolong Zha;Miyuki Koshimura;Hiroshi Fujita
在各个领域的许多组合问题都可以转化为最大可满足性问题。尽管一般问题很难解决，但是越来越多的实际问题是可以解决的，因为人们已经投入了大量的精力来开发高效的求解器。约束编码的艺术与为MaxSAT设计算法的艺术同样重要。本文基于模算法的思想，提出了几种将伪布尔约束转化为合合范式（CNF）公式中布尔可满足性问题的编码方法，这些方法只对每一个唯一的权值组合生成辅助变量。这些技术在编码和解决MaxSAT问题方面是有效的。特别是，我们的求解器在2010年至2012年期间获得了部分MaxSAT工业类别的奖项，并在2017年MaxSAT评估的主要加权轨道中排名第二。我们证明了编码的正确性和伪多项式空间复杂度，并给出了模算法基选择的启发式。实验结果表明，我们的编码对约束进行了紧凑的编码，并且得到的子句可以由最先进的SAT求解器有效地处理。
Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is-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.