Loading...
Improvements to core-guided binary search for MaxSAT
Date
2012
Abstract
Maximum Satisfiability (MaxSAT) and its weighted variants are wellknown optimization formulations of Boolean Satisfiability (SAT). Motivated by practical applications, recent years have seen the development of core-guided algorithms for MaxSAT. Among these, core-guided binary search with disjoint cores (BCD) represents a recent robust solution. This paper identifies a number of inefficiencies in the original BCD algorithm, related with the computation of lower and upper bounds during the execution of the algorithm, and develops solutions for them. In addition, the paper proposes two additional novel techniques, which can be implemented on top of core-guided MaxSAT algorithms that maintain both lower and upper bounds. Experimental results, obtained on representative problem instances, indicate that the proposed optimizations yield significant performance gains, and allow solving more problem instances.
Supervisor
Description
peer-reviewed
Publisher
Citation
Files
Keywords
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI), FCT