You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

QMaxSAT: A Partial Max-SAT Solver

Subtitle: System description

Article type: Research Article

Authors: Koshimura, Miyuki; * | Zhang, Tong | Fujita, Hiroshi | Hasegawa, Ryuzo

Affiliations: Department of Informatics, Graduate School of Information Science and Electrical Engineering, Kyushu University, Fukuoka, Japan. E-mails: [email protected], [email protected], [email protected], [email protected]

Note: [*] This work was supported by JSPS KAKENHI (20240003).

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

DOI: 10.3233/SAT190091

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 95-100, 2012

Received 1 January 2011
|
Revision received 1 June 2011
|
Published: 1 January 2012
Get PDF open access

Abstract

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.

Show more