Tags:constraint programming, core-guided, lazy clause generation and MaxSAT
Abstract:
Core Guided Maximum Satisfiability (MaxSAT) solvers are the state of the art approaches to finding optimal solutions to maximum satisfiability problems. While Core Boosted MaxSAT solvers provide the state of the art for quickly finding good solution to maximum satisfiability problems. In this paper we explore the use of core-guided and core-boosted methods for constraint programming solvers with explanation. Experimental results show for certain classes of problems core-guided search can significantly outperform traditional branch-and-bound solving approaches for CP problems to optimality. Meanwhile for many classes of problems core-boosted search significantly improves anytime CP optimization performance.