Unsatisfiable core learning for Chuffed

Unsatisfiable core learning for Chuffed: Improving the performance of Chuffed, a Lazy-Clause-Generation solver, by using machine learning to predict unsatisfiable cores

van Driel, R.A. (TU Delft Electrical Engineering, Mathematics and Computer Science)

Yorke-Smith, N. (mentor)
Verwer, S.E. (graduation committee)
Roos, S. (graduation committee)

Delft University of Technology

Computer Science

2020-07-24

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.

Constraint Programming (CP)
Propositional satisfiability (SAT)
Chuffed
graph convolutional neural networks
Variable State Independent Sum
machine learning
Lazy Clause Generation

http://resolver.tudelft.nl/uuid:18359282-e769-47d5-ac62-4ee6e1ec454e

Student theses

master thesis

© 2020 R.A. van Driel