Improving Unsatisfiability-Based Algorithms for Boolean Optimization

Abstract Recently, several unsatisfiability-based algorithms have been proposed for Maximum Satisfiability (MaxSAT) and other Boolean Optimization problems. These algorithms are based on being able to iteratively identify and relax unsatisfiable sub-formulas with the use of fast Boolean satisfiability solvers. It has been shown that this approach is very effective for several classes of instances, but it can perform poorly on others for which classical Boolean optimization algorithms find it easy to solve. This paper proposes the use of Pseudo-Boolean Optimization (PBO) solvers as a preprocessor for unsatisfiability-based algorithms in order to increase its robustness. Moreover, the use of constraint branching, a well-known technique from Integer Linear Programming, is also proposed into the unsatisfiability-based framework. Experimental results show that the integration of these features in an unsatisfiability-based algorithm results in an improved and more effective solver for Boolean optimization problems.

Authors

• Vasco Manquinho
• Ruben Martins
• Inês Lynce

Keywords

No keywords are indexed for this paper.