Unsatisfiable core learning for Chuffed

Abstract

Solving propositional satisfiability (SAT) and constraint programming (CP) instances has been a fundamental part of a wide range of modern applications. For this reason a lot of research went into improving the efficiency of modern SAT and CP solvers. Recently much of this research has gone into exploring the possibilities of integrating machine learning approaches with these solvers. However, with hybrid solvers, which combine both SAT and CP, dominating recent benchmarks it is surprising that no research has been done yet to apply those machine learning approach to improve hybrid solvers.This research proposes using a machine learning technique called unsatisfiable core learning to improve the performance of the Lazy Clause Generation solver Chuffed. The approach developed fort his study uses a Graph Convolutional Network model, which is trained on a dataset containing unsatisfiable instances. This machine learning model is then used for predicting unsatisfiable cores on CP instances and the predictions are used to initialise the activity score of the Variable State Independent Sum heuristic which is incorporated in Chuffed. The resulting approach managed to consistently solve a set of Multi-mode Resource-Constrained Project Scheduling instances 2.5% faster on average.These results indicate that, while this technique was originally developed for SAT, it can also be used to improve hybrid SAT/CP solvers.