We describe a new exact procedure, inspired on recent works on tableaux, for simultaneously solving MaxSAT and MinSAT. The main novelty of our procedure is that it implements a clause branching rule that preserves both the minimum and the maximum number of clauses than can be unsatisfied. Moreover, we prove the correctness of the procedure, and provide a review of the different types of branchings which are available for MaxSAT and MinSAT. We also give some preliminary experimental results that show that the new branching rule, when implemented into an existing branch-and-bound MaxSAT solver, produces substantial gains on industrial instances of the MaxSAT Evaluation.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com