QMaxSAT: A Partial Max-SAT Solver
QMaxSAT: A Partial Max-SAT Solver
复制标题
DOI：
10.3233/sat190091
复制
发表时间：
2012-07
期刊：
影响因子：
--
通讯作者：
Miyuki Koshimura;Tong Zhang;H. Fujita;R. Hasegawa
中科院分区：
文献类型：
--
作者：
Miyuki Koshimura;Tong Zhang;H. Fujita;R. Hasegawa
我们提出了一个部分Max-SAT求解器QMaxSAT使用CNF编码的布尔基数约束。旧版本0.1是通过调整基于CDCL的SAT求解器MiniSat来管理基数约束而获得的。在2010年Max-SAT评估的部分Max-SAT类别中，它在工业子类别中排名第一，在精心制作的子类别中排名第二。新版本0.2是通过修改版本0.1以减少基数编码的子句数量而获得的。我们通过求解2010年Max-SAT评估中的Max-SAT实例来比较这两个版本。
We present a partial Max-SAT solver QMaxSAT which uses CNF encoding of Boolean cardinality constraints. The old version 0.1 was obtained by adapting a CDCL based SAT solver MiniSat to manage cardinality constraints. It was placed rst in the industrial subcategory and second in the crafted subcategory of partial Max-SAT category of the 2010 Max-SAT Evaluation. The new version 0.2 is obtained by modifying version 0.1 to decrease the number of clauses for the cardinality encoding. We compare the two versions by solving Max-SAT instances taken from the 2010 Max-SAT Evaluation.