Towards Unsatisfiable Core Learning for Chuffed

Ronald van Driel, N. Yorke-Smith

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

13 Downloads (Pure)


Contemporary research explores the possibilities of integrating machine learning (ML) approaches with traditional combinatorial optimisation solvers. Since optimisation hybrid solvers, which combine propositional satisfiability (SAT) and constraint programming (CP), dominate recent benchmarks, it is surprising that the literature has paid limited attention to machine learning approaches for hybrid CP–SAT solvers. We identify a recent technique in the SAT literature called unsatisfiable core learning as promising to improve the performance of the hybrid CP–SAT lazy clause generation solver Chuffed. We leverage a graph convolutional network (GCN) model, trained on an adapted version of the MiniZinc benchmark suite. The GCN predicts which variables belong to an unsatisfiable cores on CP instances; these predictions are used to initialise the activity score of Chuffed’s Variable-State Independent Decaying Sum (VSIDS) heuristic. We benchmark the ML-aided Chuffed on the MiniZinc benchmark suite and find a robust 2.5% gain over baseline Chuffed on MRCPSP instances. This paper thus presents the first, to our knowledge, successful application of machine learning to improve hybrid CP–SAT solvers, a step towards improved automatic solving of CP models.
Original languageEnglish
Title of host publicationWorking Notes of the CP'20 Workshop on Progress Towards the Holy Grail
Number of pages10
Publication statusPublished - Sep 2020
EventCP'20 Workshop on Progress Towards the Holy Grail - Louvain-la-Neuve, Belgium
Duration: 1 Sep 20201 Sep 2020


WorkshopCP'20 Workshop on Progress Towards the Holy Grail


Dive into the research topics of 'Towards Unsatisfiable Core Learning for Chuffed'. Together they form a unique fingerprint.

Cite this