QMaxSAT: A Partial Max-SAT Solver

Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, Ryuzo Hasegawa


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 first 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.


partial Max-SAT solver, Boolean cardinality constraints, CDCL solver

Full Text:



  • There are currently no refbacks.